Email Gateway (Aug 18 2022 at 14:02): Email Gateway (Aug 18 2022 at 14:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Sigurd,
in "show" statements you should refrain from using the plain metalogic
connectives ==> and !! -- they are used by the Isar framework; the
solution is to internalize ==> and !! into proper Isar text (assume for
==>, fix for !!), as follows:
definition "C a b \<longleftrightarrow> b < a"
lemma a:
shows "C u u \<Longrightarrow> True"
and "True \<Longrightarrow> C u u"
proof -
assume "C u u" show True ..
next
assume True show "C u u" sorry
qed
Hope this helps
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC