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.
Poly/ML RTS version PPC-4.1.3 (12:32:32 Dec 21 2004)
Copyright (c) 2002 CUTS and contributors.
Running with heap parameters
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
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