*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] How do I do stone age interaction?*From*: Makarius <makarius at sketis.net>*Date*: Mon, 6 Dec 2010 21:17:24 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4CFD26E1.3090606@rsise.anu.edu.au>*References*: <1291650056496@names.co.uk> <alpine.LNX.1.10.1012061659070.11210@atbroy100.informatik.tu-muenchen.de> <4CFD26E1.3090606@rsise.anu.edu.au>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Mon, 6 Dec 2010, Jeremy Dawson wrote:

The ML layer certainly helps you perform proofs effectively - just by way of example here is something I wrote this afternoon, which I understand cannot be done in Isar fun in_tac sg st = (rtac insertI1 ORELSE' (rtac insertI2 THEN' in_tac)) sg st ; val _ = qed_goalw "inv_rule_aidps" CI_Rls.thy (rule_defs @ rule_lists) "inv_rule_set (PC ` aidps)" (fn _ => [ Simp_tac 1, rewtac inv_rule_set_def, Safe_tac, (TRYALL (EVERY' [rtac exI, rtac conjI, rtac refl])), (TRYALL (EVERY' [rtac drl.singleI, in_tac])),

The naked ML toplevel lacks the formal Isabelle context, which means you can hardly do anything useful, e.g. being able to parse/print expressions always requires a proper context.If "proper context" means something of the type Proof.context, then this isn't so - the "read" function implicitly uses an old style "theory context" only

I'm not sure if I understand this right, but at the ML level I certainlyget all the HOL syntax and theorems - note, though, if you're using"new-style" theory files, then to get theorems derived from the theoryfile as ML identifiers you need to use the "use_legacy_bindings"function.

Makarius

**Follow-Ups**:**Re: [isabelle] How do I do stone age interaction?***From:*Jeremy Dawson

**References**:**Re: [isabelle] How do I do stone age interaction?***From:*mark

**Re: [isabelle] How do I do stone age interaction?***From:*Makarius

**Re: [isabelle] How do I do stone age interaction?***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] How do I do stone age interaction?
- Next by Date: Re: [isabelle] How do I do stone age interaction?
- Previous by Thread: Re: [isabelle] How do I do stone age interaction?
- Next by Thread: Re: [isabelle] How do I do stone age interaction?
- Cl-isabelle-users December 2010 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