--- a/ex/Term.thy Tue May 03 11:30:09 1994 +0200
+++ b/ex/Term.thy Tue May 03 15:48:19 1994 +0200
@@ -10,8 +10,11 @@
*)
Term = List +
-types term 1
+
+types 'a term
+
arities term :: (term)term
+
consts
Term :: "'a node set set => 'a node set set"
Rep_Term :: "'a term => 'a node set"
@@ -22,6 +25,7 @@
Term_rec ::
"['a node set, ['a node set , 'a node set, 'b list]=>'b] => 'b"
term_rec :: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
+
rules
Term_def "Term(A) == lfp(%Z. A <*> List(Z))"
(*faking a type definition for term...*)