removal of obsolete type-declaration syntax
authorlcp
Tue, 03 May 1994 15:48:19 +0200
changeset 72 30e80f028c57
parent 71 9e9feb5f15dc
child 73 8129641e90ab
removal of obsolete type-declaration syntax
ex/Simult.thy
ex/Term.thy
--- a/ex/Simult.thy	Tue May 03 11:30:09 1994 +0200
+++ b/ex/Simult.thy	Tue May 03 15:48:19 1994 +0200
@@ -12,8 +12,12 @@
 *)
 
 Simult = List +
-types tree,forest 1
-arities tree,forest :: (term)term
+
+types    'a tree
+         'a forest
+
+arities  tree,forest :: (term)term
+
 consts
   Part        :: "['a set, 'a=>'a] => 'a set"
   TF          :: "'a node set set => 'a node set set"
--- 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...*)