Re: [isabelle] Get an ML value from a theory context



sternk at ubuntu:~/test$ wget
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011_bundle_x86-linux.tar.gz
  sternk at ubuntu:~/test$ tar xzf Isabelle2011_bundle_x86-linux.tar.gz
  sternk at ubuntu:~/test$ ./Isabelle2011/bin/isabelle-process HOL

This gets you into the internal system toplevel, which is not suitable for most applications nowadays. Instead you want to write your ML literally inside a theory context like this:

theory Scratch
imports Main
begin

ML {*
  Datatype.get_info @{theory} @{type_name nat}
*}

end

Note the use of antiquotations @{theory} and @{type_name ...} to refer to formal entities from the context.

See also Chapter 0 of the Implementation manual for basic examples, as well as the Programming Tutorial (aka Cookbook).

Alex





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