Re: [isabelle] antiquotations



On Thu, 21 Feb 2008, Jeremy Dawson wrote:

> At present I have a function modify_ss (of type  : MetaSimplifier.simpset ->
> MetaSimplifier.simpset).
> 
> It is used in a further function
> 
> fun modified_ss () = modify_ss (simpset ()) ;
> 
> Now I observe that
> 
> val simpset = simpset_of o ML_Context.the_context;
> 
> and given the previous remarks about using the_context () I assume that you
> wouldn't approve of using simpset (), either.  Is that correct?

Yes, the simpset() form is indeed a legacy feature.  If it occurs in 
one-shot scripts, it can usually be replaced by the static version 
@{simpset}; the same for @{claset} or @{clasimpset}.

Your application sounds more like requiring a run-time context, though. So 
assuming you have a proper value (ctxt: Proof.context) already, you may 
get the simpset component like this:

  local_simpset_of ctxt

and then add your stuff to the result.


> How do I define modified_ss in the approved way - using antiquotations 
> as and where appropriate ?

Most likely, no antiquotations will get involved here, because you are 
working only with a runtime context.  You still need to get hold of that, 
i.e. ``by induction over the structure of your code'' as explained 
earlier.


	Makarius





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