Re: [isabelle] HOL quantifiers in intro rules


Am Donnerstag, den 20.11.2014, 10:43 +0100 schrieb Tobias Nipkow:
> One reason I sometimes use HOL connectives in premises is that it is more 
> convenient for forward reasoning: you can write closed_Inter[OF ...]. I don't 
> know how to do this as compactly if the premise is not atomic.

good point. I also often want a non-atomic OF.

I might be wrong, butmaybe this is what COMP was about?
        New in Isabelle2013 (February 2013)
        Discontinued obsolete attribute "COMP".  Potential
        use regular rule composition via "OF" / "THEN", or explicit
        structure instead.
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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