*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] antiquotations*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Fri, 22 Feb 2008 09:11:23 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>*In-reply-to*: <47BE318E.6070607@rsise.anu.edu.au>*References*: <478AAC94.3030404@rsise.anu.edu.au> <478B2940.5020107@informatik.tu-muenchen.de> <478BEE3B.2000007@rsise.anu.edu.au> <478C8265.2010202@in.tum.de> <478D322C.7010001@rsise.anu.edu.au> <478DB7F0.7080604@in.tum.de> <478E6F17.9000100@rsise.anu.edu.au> <478E816D.9010606@in.tum.de> <478EF53A.9070809@rsise.anu.edu.au> <Pine.LNX.4.63.0801241542360.18967@atbroy100.informatik.tu-muenchen.de> <47ABC81B.3090608@rsise.anu.edu.au> <Pine.LNX.4.63.0802081405450.9643@atbroy100.informatik.tu-muenchen.de> <47AF877C.4050205@rsise.anu.edu.au> <47B04E56.7010901@in.tum.de> <47BE318E.6070607@rsise.anu.edu.au>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Dear Jeremy,

thanks - OK, now I've got a function of a type which hopefully doesn'tuse any impure features:# val addsm = fn : Context.theory -> Context.theory Now, what do I do with it? (Your email showed an example using setup {* ... : theory -> theory *},but I have this function, and want to use it, inside an ML file which isto be "used" by a theory)

That depends on the application.

- install new commands, methods and attributes - Do something else (definitions, proofs or anything) at a specific point.

Alex

**References**:**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Makarius

**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Alexander Krauss

**Re: [isabelle] antiquotations***From:*Jeremy Dawson

- Previous by Date: [isabelle] debugging Isar
- Next by Date: Re: [isabelle] debugging Isar
- Previous by Thread: Re: [isabelle] antiquotations
- Next by Thread: Re: [isabelle] antiquotations
- Cl-isabelle-users February 2008 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