# HG changeset patch
# User lcp
# Date 767972899 -7200
# Node ID 30e80f028c577e266d63ed23328fb99eb818d112
# Parent  9e9feb5f15dc26405005f6f4c9b82fa54349c8c3
removal of obsolete type-declaration syntax

diff -r 9e9feb5f15dc -r 30e80f028c57 ex/Simult.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"
diff -r 9e9feb5f15dc -r 30e80f028c57 ex/Term.thy
--- 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...*)