Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange behavior in isabelle 2009, *** Failed ...

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: Apr 20 2024 at 04:19 UTC