# HG changeset patch
# User lcp
# Date 763920169 -3600
# Node ID 934a58983311cb00888041d43c9bb6006b6b39e3
# Parent  2e9a86203d5977f7ec62ef88a70ace3dfb8414a6
new type declaration syntax instead of numbers

diff -r 2e9a86203d59 -r 934a58983311 LList.thy
--- a/LList.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/LList.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -24,8 +24,13 @@
 *)
 
 LList = Gfp + List +
-types llist 1
-arities llist :: (term)term
+
+types
+  'a llist
+
+arities
+   llist :: (term)term
+
 consts
   LList      :: "'a node set set => 'a node set set"
   LListD_Fun :: 
diff -r 2e9a86203d59 -r 934a58983311 Nat.thy
--- a/Nat.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/Nat.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -9,9 +9,14 @@
 *)
 
 Nat = WF +
-types ind,nat 0
-arities ind,nat :: term
-        nat :: ord
+
+types
+  ind
+  nat
+
+arities
+  ind,nat :: term
+  nat     :: ord
 
 consts
   Zero_Rep	:: "ind"
diff -r 2e9a86203d59 -r 934a58983311 Prod.thy
--- a/Prod.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/Prod.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -11,29 +11,32 @@
 *)
 
 Prod = Set +
+
 types   
-	"*"  2        (infixr 20)
-        unit
+  ('a,'b) "*"          (infixr 20)
+  unit
+
 arities 
-   "*"      :: (term,term)term
-   unit     :: term
+  "*"      :: (term,term)term
+  unit     :: term
+
 consts
-   Pair_Rep :: "['a,'b] => ['a,'b] => bool"
-   Prod	    :: "('a => 'b => bool)set"
-   Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
-   Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
-   fst	    :: "'a * 'b => 'a"
-   snd	    :: "'a * 'b => 'b"
-   split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
-   prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
-   Pair	    :: "['a,'b] => 'a * 'b"
-   "@Tuple" :: "args => 'a*'b"			("(1<_>)")
-   Sigma    :: "['a set, 'a => 'b set] => ('a*'b)set"
+  Pair_Rep :: "['a,'b] => ['a,'b] => bool"
+  Prod	   :: "('a => 'b => bool)set"
+  Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
+  Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
+  fst	   :: "'a * 'b => 'a"
+  snd	   :: "'a * 'b => 'b"
+  split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
+  prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
+  Pair	   :: "['a,'b] => 'a * 'b"
+  "@Tuple" :: "args => 'a*'b"			("(1<_>)")
+  Sigma    :: "['a set, 'a => 'b set] => ('a*'b)set"
 
-   Unit	    :: "bool set"
-   Rep_Unit :: "unit => bool"
-   Abs_Unit :: "bool => unit"
-   Unity    :: "unit"					("<>")
+  Unit	   :: "bool set"
+  Rep_Unit :: "unit => bool"
+  Abs_Unit :: "bool => unit"
+  Unity    :: "unit"					("<>")
 
 translations
 
diff -r 2e9a86203d59 -r 934a58983311 Sum.thy
--- a/Sum.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/Sum.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -7,17 +7,23 @@
 *)
 
 Sum = Prod +
-types   "+" 2      (infixl 10)
-arities "+"     :: (term,term)term
+
+types
+  ('a,'b) "+"		      (infixl 10)
+
+arities
+  "+"      :: (term,term)term
+
 consts
-   Inl_Rep	:: "['a,'a,'b,bool] => bool"
-   Inr_Rep	:: "['b,'a,'b,bool] => bool"
-   Sum		:: "(['a,'b,bool] => bool)set"
-   Rep_Sum	:: "'a + 'b => (['a,'b,bool] => bool)"
-   Abs_Sum	:: "(['a,'b,bool] => bool) => 'a+'b"
-   Inl		:: "'a => 'a+'b"
-   Inr		:: "'b => 'a+'b"
-   sum_case	:: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+  Inl_Rep  :: "['a,'a,'b,bool] => bool"
+  Inr_Rep  :: "['b,'a,'b,bool] => bool"
+  Sum      :: "(['a,'b,bool] => bool)set"
+  Rep_Sum  :: "'a + 'b => (['a,'b,bool] => bool)"
+  Abs_Sum  :: "(['a,'b,bool] => bool) => 'a+'b"
+  Inl	   :: "'a => 'a+'b"
+  Inr	   :: "'b => 'a+'b"
+  sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+
 rules
   Inl_Rep_def	"Inl_Rep == (%a. %x y p. x=a & p)"
   Inr_Rep_def	"Inr_Rep == (%b. %x y p. y=b & ~p)"
diff -r 2e9a86203d59 -r 934a58983311 Univ.thy
--- a/Univ.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/Univ.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -12,8 +12,13 @@
 *)
 
 Univ = Arith +
-types   node 1
-arities node :: (term)term
+
+types
+  'a node
+
+arities
+  node :: (term)term
+
 consts
   Least     :: "(nat=>bool) => nat"    (binder "LEAST " 10)
 
diff -r 2e9a86203d59 -r 934a58983311 llist.thy
--- a/llist.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/llist.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -24,8 +24,13 @@
 *)
 
 LList = Gfp + List +
-types llist 1
-arities llist :: (term)term
+
+types
+  'a llist
+
+arities
+   llist :: (term)term
+
 consts
   LList      :: "'a node set set => 'a node set set"
   LListD_Fun :: 
diff -r 2e9a86203d59 -r 934a58983311 nat.thy
--- a/nat.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/nat.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -9,9 +9,14 @@
 *)
 
 Nat = WF +
-types ind,nat 0
-arities ind,nat :: term
-        nat :: ord
+
+types
+  ind
+  nat
+
+arities
+  ind,nat :: term
+  nat     :: ord
 
 consts
   Zero_Rep	:: "ind"
diff -r 2e9a86203d59 -r 934a58983311 prod.thy
--- a/prod.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/prod.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -11,29 +11,32 @@
 *)
 
 Prod = Set +
+
 types   
-	"*"  2        (infixr 20)
-        unit
+  ('a,'b) "*"          (infixr 20)
+  unit
+
 arities 
-   "*"      :: (term,term)term
-   unit     :: term
+  "*"      :: (term,term)term
+  unit     :: term
+
 consts
-   Pair_Rep :: "['a,'b] => ['a,'b] => bool"
-   Prod	    :: "('a => 'b => bool)set"
-   Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
-   Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
-   fst	    :: "'a * 'b => 'a"
-   snd	    :: "'a * 'b => 'b"
-   split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
-   prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
-   Pair	    :: "['a,'b] => 'a * 'b"
-   "@Tuple" :: "args => 'a*'b"			("(1<_>)")
-   Sigma    :: "['a set, 'a => 'b set] => ('a*'b)set"
+  Pair_Rep :: "['a,'b] => ['a,'b] => bool"
+  Prod	   :: "('a => 'b => bool)set"
+  Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
+  Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
+  fst	   :: "'a * 'b => 'a"
+  snd	   :: "'a * 'b => 'b"
+  split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
+  prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
+  Pair	   :: "['a,'b] => 'a * 'b"
+  "@Tuple" :: "args => 'a*'b"			("(1<_>)")
+  Sigma    :: "['a set, 'a => 'b set] => ('a*'b)set"
 
-   Unit	    :: "bool set"
-   Rep_Unit :: "unit => bool"
-   Abs_Unit :: "bool => unit"
-   Unity    :: "unit"					("<>")
+  Unit	   :: "bool set"
+  Rep_Unit :: "unit => bool"
+  Abs_Unit :: "bool => unit"
+  Unity    :: "unit"					("<>")
 
 translations
 
diff -r 2e9a86203d59 -r 934a58983311 sum.thy
--- a/sum.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/sum.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -7,17 +7,23 @@
 *)
 
 Sum = Prod +
-types   "+" 2      (infixl 10)
-arities "+"     :: (term,term)term
+
+types
+  ('a,'b) "+"		      (infixl 10)
+
+arities
+  "+"      :: (term,term)term
+
 consts
-   Inl_Rep	:: "['a,'a,'b,bool] => bool"
-   Inr_Rep	:: "['b,'a,'b,bool] => bool"
-   Sum		:: "(['a,'b,bool] => bool)set"
-   Rep_Sum	:: "'a + 'b => (['a,'b,bool] => bool)"
-   Abs_Sum	:: "(['a,'b,bool] => bool) => 'a+'b"
-   Inl		:: "'a => 'a+'b"
-   Inr		:: "'b => 'a+'b"
-   sum_case	:: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+  Inl_Rep  :: "['a,'a,'b,bool] => bool"
+  Inr_Rep  :: "['b,'a,'b,bool] => bool"
+  Sum      :: "(['a,'b,bool] => bool)set"
+  Rep_Sum  :: "'a + 'b => (['a,'b,bool] => bool)"
+  Abs_Sum  :: "(['a,'b,bool] => bool) => 'a+'b"
+  Inl	   :: "'a => 'a+'b"
+  Inr	   :: "'b => 'a+'b"
+  sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+
 rules
   Inl_Rep_def	"Inl_Rep == (%a. %x y p. x=a & p)"
   Inr_Rep_def	"Inr_Rep == (%b. %x y p. y=b & ~p)"
diff -r 2e9a86203d59 -r 934a58983311 univ.thy
--- a/univ.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/univ.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -12,8 +12,13 @@
 *)
 
 Univ = Arith +
-types   node 1
-arities node :: (term)term
+
+types
+  'a node
+
+arities
+  node :: (term)term
+
 consts
   Least     :: "(nat=>bool) => nat"    (binder "LEAST " 10)