*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] antiquotations*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 22 Feb 2008 13:21:02 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>*In-reply-to*: <47B04E56.7010901@in.tum.de>*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>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Alexander Krauss wrote:

A further question from a previous email (the answer given then was to use a different function) : bind_thm(s) seems to sometimes work (in the sense of storing a theorem in the database so that it can be effectively retrieved later). Why is this? What is the difference between bind_thm and the function I was told to use (ie, PureThy.add_thmss)?You can read the answer from its type: bind_thms : string * Thm.thm list -> unit PureThy.add_thmss : ((bstring * Thm.thm list) * Thm.attribute list) list -> Context.theory -> Thm.thm list list * Context.theory Since bind_thms is impure, it can only update some global reference hanging around. This is incompatible with paralellism. At the moment it may work sometimes, but it is guaranteed to break sooner or later.

Dear Alexander,

# val addsm = fn : Context.theory -> Context.theory

(Your email showed an example using setup {* ... : theory -> theory *},

regards, Jeremy Dawson

**Follow-Ups**:**Re: [isabelle] antiquotations***From:*Alexander Krauss

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

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

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

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

- Previous by Date: Re: [isabelle] schematic variables in lemmas-command
- Next by Date: [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