Re: [isabelle] Define records in ML?



On Mon, 13 Nov 2006, Thomas Bleher wrote:

> I looked at 
> https://cgi.cse.unsw.edu.au/~formalmethods/wiki/isabelle/index.cgi/ProgrammingIsabelle 

Maybe you want to take a look at the "implementation" manual, which is 
part of recent development snapshots.  (It is only about 25% finished, but 
the already existing parts are in an orderly state.)


> However, the next command then fails with
>   "exception TERM raised: Stale theory encountered: {<long list of theories>}"
> 
> Which magic incantation do I have to use to add a typedecl (or anything
> else) to the current theory?

The deeper problem here is what ``current theory'' refers to.  The "Stale 
theory encountered" indicates that some no longer valid theory value was 
involved.  Normally you just work with (fn thy => ...) abstractly -- where 
the function body uses thy in a strictly linear fashion.  Then plug in the 
result as Toplevel.theory transaction.  Alternatively you may experiment 
with the 'setup' command in ProofGeneral/Isar mode.  For example:

  setup {* TypedefPackage.add_typedecls [("foo", ["'a", "'b"], NoSyn)] *}

  typ "(nat, bool) foo"

Paradoxically, it is much easier to work with ML in the Isar interaction 
mode, instead of the raw ML toplevel.  (Sometimes some low-level output 
only occurrs in the *isabelle* buffer in ProofGeneral.)


	Makarius





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