*To*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] A constant become a free variable*From*: Makarius <makarius at sketis.net>*Date*: Wed, 4 Dec 2013 16:17:31 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <op.w7kpl9t8ule2fv@cardamome>*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> <op.w7kpl9t8ule2fv@cardamome>*User-agent*: Alpine 2.11 (LSU 23 2013-08-11)

On Wed, 4 Dec 2013, Yannick Duchêne (Hibou57) wrote:

Le Wed, 04 Dec 2013 16:00:56 +0100, Makarius <makarius at sketis.net> a écrit: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.Does that mean substitution/simplification is not expressed with “==”but “=” instead ? I always though “==” was the standard for that purposewith logic.

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

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

- Previous by Date: Re: [isabelle] A constant become a free variable
- Next by Date: Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context
- Previous by Thread: Re: [isabelle] A constant become a free variable
- Next by Thread: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context
- 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