[isabelle-dev] Unexpected auto indent in 13a1081961d2

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Sep 3 16:08:05 CEST 2017

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?



PGP available:
-------------- next part --------------
theory Foo
imports Main

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
  case False
  with that show ?thesis
  by simp
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170903/e069e176/attachment.asc>

More information about the isabelle-dev mailing list