Dear all, the attached theory is the (unexpected) result of typing its content naively and relying on auto indent.
Do others experience the same or is it maybe a settings problem?
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
theory Foo imports Main begin definition I :: "'a \<Rightarrow> 'a" where "I x = x" definition K :: "'b \<Rightarrow> 'a \<Rightarrow> 'a" where "K x = I" lemma K_apply: "K y x = x" by (simp add: K_def I_def) lemma nonsense: "2 * n div 2 = n" if "even n" for n :: nat proof (cases "even n") case True then show ?thesis by simp next case False with that show ?thesis by simp qed
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
