*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Accessing lift_definition from the ML-level*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Fri, 10 Oct 2014 11:51:36 +0200*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1410082312060.10395@lxbroy10.informatik.tu-muenchen.de>*References*: <B24807B6-CE22-4F9C-936A-9A309E4B2E44@uibk.ac.at> <4A1A348A-B908-4FFB-84E2-0D661E3EA4A8@uibk.ac.at> <alpine.LNX.2.00.1410082312060.10395@lxbroy10.informatik.tu-muenchen.de>

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é

**References**:**[isabelle] Accessing lift_definition from the ML-level***From:*René Thiemann

**Re: [isabelle] Accessing lift_definition from the ML-level***From:*René Thiemann

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

- Previous by Date: [isabelle] New AFP entry: Probability Density Functions
- Next by Date: Re: [isabelle] Sublocale, subclass and execution.
- Previous by Thread: Re: [isabelle] Accessing lift_definition from the ML-level
- Next by Thread: [isabelle] linear programming
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list