Re: [isabelle] Replacing COMP

On Tue, 30 Jul 2013, Andreas Lochbihler wrote:

2. Note that "asm" as a premise in the assumes is redundant in lift_foo. The following lemma is equivalent:

 lift_foo': "[| concl; asm |] ==> concl"

Looking here again, this note by Andreas seems important.


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