Re: [isabelle] My unforgivable soundness issue with a locale
Le Mon, 23 Dec 2013 12:19:43 +0100, Johannes Hölzl
<hoelzl at in.tum.de> a écrit:
Am Sonntag, den 22.12.2013, 18:51 +0100 schrieb Yannick Duchêne
By the way, a question aside: is there a way to refer to a proposition
from another proposition? I mean so that I would not have to copy/paste
the premiss of “(text of B) ⟹ (text of A)” and just refer to B, as “B ⟹
(text of A)” instead of the latter.
I'm not sure for the locale syntax, but when writing lemmas you an
use ?X patterns:
lemma assumes "B" (is ?B) shows "?B ==> A"
I already tried this one. It seems to be allowed by Isar‑Ref, but Isabelle
reject it with this message: “Illegal term bindings in context element”.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and