*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] A constant become a free variable*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Wed, 04 Dec 2013 16:07:11 +0100*Organization*: Ada @ Home*References*: <op.w7j82jjfule2fv@cardamome> <alpine.LSU.2.11.1312041300550.13772@macbroy21.informatik.tu-muenchen.de> <op.w7ko6lu8esn74s@cardamome> <alpine.LSU.2.11.1312041558590.4831@macbroy21.informatik.tu-muenchen.de>*User-agent*: Opera Mail/12.16 (Linux)

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.

-- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**Follow-Ups**:**Re: [isabelle] A constant become a free variable***From:*Makarius

**References**:**[isabelle] A constant become a free variable***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] A constant become a free variable***From:*Makarius

**Re: [isabelle] A constant become a free variable***From:*Yannick

**Re: [isabelle] A constant become a free variable***From:*Makarius

- Previous by Date: Re: [isabelle] A constant become a free variable
- Next by Date: Re: [isabelle] A constant become a free variable
- Previous by Thread: Re: [isabelle] A constant become a free variable
- Next by Thread: Re: [isabelle] A constant become a free variable
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list