adapted type definition to new syntax
authorclasohm
Thu, 17 Mar 1994 11:27:29 +0100
changeset 49 9f35f2744fa8
parent 48 21291189b51e
child 50 2e9a86203d59
adapted type definition to new syntax
HOL.thy
List.thy
Prod.thy
Set.thy
ex/MT.thy
ex/mt.thy
hol.thy
prod.thy
set.thy
--- a/HOL.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/HOL.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -18,7 +18,7 @@
   term
 
 types
-  bool 0
+  bool
   letbinds, letbind 0
   case_syn,cases_syn 0
 
--- a/List.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/List.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -13,7 +13,7 @@
 List = Sexp +
 
 types
-  list 1
+  'a list
 
 arities
   list :: (term) term
--- a/Prod.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/Prod.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -13,7 +13,7 @@
 Prod = Set +
 types   
 	"*"  2        (infixr 20)
-        unit 0
+        unit
 arities 
    "*"      :: (term,term)term
    unit     :: term
--- a/Set.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/Set.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -7,7 +7,7 @@
 Set = Ord +
 
 types
-  set 1
+  'a set
 
 arities
   set :: (term) term
--- a/ex/MT.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/ex/MT.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -16,19 +16,19 @@
 MT = Gfp +
 
 types 
-  Const 0
+  Const
 
-  ExVar 0
-  Ex 0
+  ExVar
+  Ex
 
-  TyConst 0
-  Ty 0
+  TyConst
+  Ty
 
-  Clos 0
-  Val 0
+  Clos
+  Val
 
-  ValEnv 0
-  TyEnv 0
+  ValEnv
+  TyEnv
 
 arities 
   Const :: term
--- a/ex/mt.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/ex/mt.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -16,19 +16,19 @@
 MT = Gfp +
 
 types 
-  Const 0
+  Const
 
-  ExVar 0
-  Ex 0
+  ExVar
+  Ex
 
-  TyConst 0
-  Ty 0
+  TyConst
+  Ty
 
-  Clos 0
-  Val 0
+  Clos
+  Val
 
-  ValEnv 0
-  TyEnv 0
+  ValEnv
+  TyEnv
 
 arities 
   Const :: term
--- a/hol.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/hol.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -18,7 +18,7 @@
   term
 
 types
-  bool 0
+  bool
   letbinds, letbind 0
   case_syn,cases_syn 0
 
--- a/prod.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/prod.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -13,7 +13,7 @@
 Prod = Set +
 types   
 	"*"  2        (infixr 20)
-        unit 0
+        unit
 arities 
    "*"      :: (term,term)term
    unit     :: term
--- a/set.thy	Wed Mar 02 12:26:55 1994 +0100
+++ b/set.thy	Thu Mar 17 11:27:29 1994 +0100
@@ -7,7 +7,7 @@
 Set = Ord +
 
 types
-  set 1
+  'a set
 
 arities
   set :: (term) term