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

sternk at ubuntu:~/test$ wget
  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

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


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).


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