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
       use regular rule composition via "OF" / "THEN", or explicit
       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.


           925,360 people so far

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