Re: [isabelle] antiquotations



Dear Jeremy,

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)

That depends on the application.

You use "setup", when you want to apply the function to the current theory at that point in the source. This can be used e.g. to

 - install new commands, methods and attributes

 - Do something else (definitions, proofs or anything) at a
   specific point.

On the other hand, if you are adding something like a method (=Isar version of a tactic), then you are usually given a theory (or a Proof.context) by the framework.

Can you describe your application (i.e. what does "addsm" do and how should it be used on a theory), then I can be more concrete.

Alex






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