Re: [isabelle] HOL quantifiers in intro rules



Hi,

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
        INCOMPATIBILITY,
        use regular rule composition via "OF" / "THEN", or explicit
        proof
        structure instead.
        
Greetings,
Joachim
        
-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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