Email Gateway (Aug 19 2022 at 16:12): Email Gateway (Aug 19 2022 at 16:12):From: Buday Gergely <gbuday@karolyrobert.hu>
Dear Martin,
please do not send us an Isabelle theory with no new lines, it is not readable.
Also it is advisable to send a self-containing, working Isabelle theory with only the necessary parts to exhibit your problem. That is also called a minimal example on the Internet.
Email Gateway (Aug 19 2022 at 16:13):From: M A <tesleft@hotmail.com>
Hi
I send with outlook.com. How to add new lines? does it mean like programming add "\r\n" at the end?
for example:
hello\r\nhello\r\n
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:13):From: M A <tesleft@hotmail.com>
Hi Buday,
i failed to add new lines in outlook.com in window.
now i send it again in firefox in ubuntu.
for example:
hello
hello
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:13):From: M A <tesleft@hotmail.com>
Hi
succeed to add new lines in ubuntu's firefox, i send again the question
failed to parse lemma when prove the following
would like to see any further usage when continuing adding letters into it
lemma mfold5 [simp]:"mfold5 f [a,b,c,d,e] x = f e (f d (f c (f b (f a x))))"
lemma mfold [simp]:"mfold f [a,b,c] x = f c (f b (f a x))"apply(simp_all)apply(auto)donelemma mfoldr [simp]:"mfoldr f [a,b,c] x = f a (f b (f c x))"apply(induct_tac x)apply(auto)donelemma mfoldl [simp]:"mfoldl f x [a,b,c] = f (f (f x a) b) c"apply(induct_tac x)apply(auto)done
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:13):From: M A <tesleft@hotmail.com>
Hi
After pressing enter again, i send again the question in ubuntu's firefox.
failed to parse lemma when prove the following
lemma mfold5 [simp]:"mfold5 f [a,b,c,d,e] x = f e (f d (f c (f b (f a x))))"
lemma mfold [simp]:"mfold f [a,b,c] x = f c (f b (f a x))"
apply(simp_all)
apply(auto)
done
Regards,
Martin
Last updated: Apr 24 2024 at 01:07 UTC