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
(Hibou57):
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"
  ...

 - Johannes

Hello Johannes,

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.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.