*To*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Subject*: Re: [isabelle] accessing ML definitions in isabelle_process*From*: Makarius <makarius at sketis.net>*Date*: Tue, 28 Apr 2015 20:35:55 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <553FCF66.1090408@aalto.fi>*References*: <553FA17B.4020002@aalto.fi> <alpine.LNX.2.00.1504281940020.19676@lxbroy10.informatik.tu-muenchen.de> <553FCF66.1090408@aalto.fi>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 28 Apr 2015, Viorel Preoteasa wrote:

Using Isabelle/ML snippets inside a proper theory context seems orientedtowards a user interface. But I need to do this in batch mode. If I usethis approach I have to create always a theory file, and then load itusing use_thy. I would need to do this for every small call that I need.

fun simplifya s ct th =

I can define this code in a ml file, except: val Set_ex_bool_eq = @{thm Set.ex_bool_eq}; val Set_all_bool_eq = @{thm Set.all_bool_eq};probably there is a way to get these theorems at the toplevel ofisabelle_processusing the context and the theory.

Makarius

**Follow-Ups**:**Re: [isabelle] accessing ML definitions in isabelle_process***From:*Viorel Preoteasa

**References**:**[isabelle] accessing ML definitions in isabelle_process***From:*Viorel Preoteasa

**Re: [isabelle] accessing ML definitions in isabelle_process***From:*Makarius

**Re: [isabelle] accessing ML definitions in isabelle_process***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] accessing ML definitions in isabelle_process
- Next by Date: Re: [isabelle] accessing ML definitions in isabelle_process
- Previous by Thread: Re: [isabelle] accessing ML definitions in isabelle_process
- Next by Thread: Re: [isabelle] accessing ML definitions in isabelle_process
- Cl-isabelle-users April 2015 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