Re: [isabelle] Accessing lift_definition from the ML-level



Dear Makarius,

>> However, now I am left with turning a Proof.state into a context again (which should be done via the provided tactic). So, is there some common function of type
>> 
>> state -> tactic -> context
>> 
>> In proof.ML I only found functions like
>> 
>> global_qed which take "Method.text_range option * bool", but no tactics.
> 
> Just syntactically, this one works out, but I did not try it on concrete
> examples:
> 
>  val term_to_string = YXML.string_of_body o Term_XML.Encode.term;
>  val typ_to_string = YXML.string_of_body o Term_XML.Encode.typ;
> 
>  fun lift_def_ml (binding, mx) ty rhs tactic lthy =
>    let
>      val method = (Method.Basic (SIMPLE_METHOD o tactic), Position.no_range);
>    in
>      lthy
>      |> Lifting_Def.lift_def_cmd
>        ((binding, SOME (typ_to_string ty), mx), term_to_string rhs, [])
>     |> Proof.global_terminal_proof (method, NONE)
>    end

thanks a lot, that works perfectly in my setting.

> I have made this a bit more canonical according to Isabelle/ML standards, concerning names and argument order. In particular, a lthy: local_theory value should not be called "ctxt".  See the "implementation" manual for further important information on Isabelle/ML.
done.

> You've put the term "ML-level of Isabelle" into the subject line.  

I'll try to use Isabelle/ML the next time.

Cheers,
René



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