[isabelle-dev] Unexpected auto indent in 13a1081961d2

[Florian Haftmann]

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
-------------- next part --------------
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
  
-------------- 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>