Re: [isabelle] My unforgivable soundness issue with a locale
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and