Re: [isabelle] Accessing lift_definition from the ML-level
>> 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
> 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 =
> val method = (Method.Basic (SIMPLE_METHOD o tactic), Position.no_range);
> |> Lifting_Def.lift_def_cmd
> ((binding, SOME (typ_to_string ty), mx), term_to_string rhs, )
> |> Proof.global_terminal_proof (method, NONE)
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.
> You've put the term "ML-level of Isabelle" into the subject line.
I'll try to use Isabelle/ML the next time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and