*To*: Walther Neuper <wneuper at ist.tugraz.at>*Subject*: Re: [isabelle] add_assoc, add.assoc and reflection*From*: Makarius <makarius at sketis.net>*Date*: Mon, 20 Apr 2015 11:05:45 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk, Andreas Pöchtrager <pand at gmx.at>*In-reply-to*: <55349F66.1070001@ist.tugraz.at>*References*: <55349F66.1070001@ist.tugraz.at>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 20 Apr 2015, Walther Neuper wrote:

Looking at val ctxt = Proof_Context.init_global @{theory Main}; Syntax.read_term ctxt "add_assoc" (* = Free ("add_assoc", "'a"): term *) Syntax.read_term ctxt "add.assoc" (* ERROR: Undefined constant: "add.assoc"*) is my assumption right, that the latter is considered outer syntax only?In other words: The latter is NOT considered to become a valid term (i.e.inner syntax) within some context ?If both questions are answered "yes", then this question comes up: How comesthat the designers of Isabelle are sure, that theorem names never shall occurin functions defined within Isabelle's function package (where functiondefinitions are terms, i.e. belong to inner syntax) ?

Makarius

**Follow-Ups**:**Re: [isabelle] add_assoc, add.assoc and reflection***From:*Walther Neuper

**References**:**[isabelle] add_assoc, add.assoc and reflection***From:*Walther Neuper

- Previous by Date: Re: [isabelle] add_assoc, add.assoc and reflection
- Next by Date: Re: [isabelle] add_assoc, add.assoc and reflection
- Previous by Thread: Re: [isabelle] add_assoc, add.assoc and reflection
- Next by Thread: Re: [isabelle] add_assoc, add.assoc and reflection
- Cl-isabelle-users April 2015 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