Re: [isabelle] antiquotations

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,

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,

thanks - OK, now I've got a function of a type which hopefully doesn't use 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 is to be "used" by a theory)


Jeremy Dawson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.