Re: [isabelle] HOL quantifiers in intro rules



On Thu, 20 Nov 2014, Joachim Breitner wrote:

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.

COMP was one of these historical relics that are better forgotten, and not unearthed again. The topic occasionally showed up on the mailing list in the past decades, just in case you want to know more about its distant past.

As a rule of thumb, uses of COMP are either very old tools, or based on general misunderstandings how the system works, or very special applications somewhere in the system infrastructure itself.


	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  925,360 people so far
----------------------------------------------------------------------------




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