Re: [isabelle] My unforgivable soundness issue with a locale



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





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