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
  

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to