Re: [isabelle] term_tvars

One suggestion is that you work directly with the ML level rather than from the Isar level: use "isabelle" rather than "Isabelle" to start up. Then use the constructors in Pure/term.ML to express terms.

~: isabelle
Poly/ML RTS version PPC-4.1.3 (12:32:32 Dec 21 2004)
Copyright (c) 2002 CUTS and contributors.
Running with heap parameters (h=81920K,ib=16384K,ip=100%,mb=20480K,mp=20%)
Mapping /Users/lcp/isabelle/heaps/polyml-4.1.3_ppc-darwin/HOL
Mapping /Users/lcp/isabelle/Repos/polyml-4.1.3/ppc-darwin/ML_dbase
Poly/ML 4.1.3 Release
> val it = () : unit
> Free ("fred", TVar (("'a",3), ["logic"]));
val it = Free ("fred", "?'a3") : Term.term
> term_tvars it;
val it = [(("'a", 3), ["logic"])] : (Term.indexname * Term.sort) list

Larry Paulson

On 23 Oct 2005, at 23:06, Sean McLaughlin wrote:

How can I get this to work?

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