Re: [isabelle] A constant become a free variable



On Wed, 4 Dec 2013, Yannick wrote:

I've just checked, and “HOL.thy” indeed says “(*admissible axiom*)”. Will try to learn to do without it.

In some sense this belongs to the "implementation" of Isabelle/HOL on top of the Isabelle/Pure framework.

These days you should hardly ever need == in Isabelle/HOL applications.

This is different to !! and ==>, which have a specific purpose to outline Natural Deduction rule schemes in a declarative manner, independently of the object-logic.


	Makarius


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