--- a/src/CCL/CCL.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/CCL/CCL.thy Thu Mar 17 17:48:37 1994 +0100
@@ -17,7 +17,7 @@
default prog
-types i 0
+types i
arities
i :: prog
--- a/src/CCL/ccl.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/CCL/ccl.thy Thu Mar 17 17:48:37 1994 +0100
@@ -17,7 +17,7 @@
default prog
-types i 0
+types i
arities
i :: prog
--- a/src/CTT/CTT.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/CTT/CTT.thy Thu Mar 17 17:48:37 1994 +0100
@@ -8,9 +8,13 @@
CTT = Pure +
-types i,t,o 0
+types
+ i
+ t
+ o
-arities i,t,o :: logic
+arities
+ i,t,o :: logic
consts
(*Types*)
--- a/src/CTT/ctt.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/CTT/ctt.thy Thu Mar 17 17:48:37 1994 +0100
@@ -8,9 +8,13 @@
CTT = Pure +
-types i,t,o 0
+types
+ i
+ t
+ o
-arities i,t,o :: logic
+arities
+ i,t,o :: logic
consts
(*Types*)
--- a/src/FOLP/IFOLP.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/FOLP/IFOLP.thy Thu Mar 17 17:48:37 1994 +0100
@@ -4,9 +4,12 @@
default term
-types p,o 0
+types
+ p
+ o
-arities p,o :: logic
+arities
+ p,o :: logic
consts
(*** Judgements ***)
--- a/src/FOLP/ifolp.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/FOLP/ifolp.thy Thu Mar 17 17:48:37 1994 +0100
@@ -4,9 +4,12 @@
default term
-types p,o 0
+types
+ p
+ o
-arities p,o :: logic
+arities
+ p,o :: logic
consts
(*** Judgements ***)
--- a/src/LCF/LCF.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/LCF/LCF.thy Thu Mar 17 17:48:37 1994 +0100
@@ -12,12 +12,15 @@
default cpo
-types tr,void 0
- "*" 2 (infixl 6)
- "+" 2 (infixl 5)
+types
+ tr
+ void
+ ('a,'b) "*" (infixl 6)
+ ('a,'b) "+" (infixl 5)
-arities fun, "*", "+" :: (cpo,cpo)cpo
- tr,void :: cpo
+arities
+ fun, "*", "+" :: (cpo,cpo)cpo
+ tr,void :: cpo
consts
UU :: "'a"
--- a/src/LCF/lcf.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/LCF/lcf.thy Thu Mar 17 17:48:37 1994 +0100
@@ -12,12 +12,15 @@
default cpo
-types tr,void 0
- "*" 2 (infixl 6)
- "+" 2 (infixl 5)
+types
+ tr
+ void
+ ('a,'b) "*" (infixl 6)
+ ('a,'b) "+" (infixl 5)
-arities fun, "*", "+" :: (cpo,cpo)cpo
- tr,void :: cpo
+arities
+ fun, "*", "+" :: (cpo,cpo)cpo
+ tr,void :: cpo
consts
UU :: "'a"
--- a/src/LK/LK.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/LK/LK.thy Thu Mar 17 17:48:37 1994 +0100
@@ -7,11 +7,17 @@
*)
LK = Pure +
+
classes term < logic
+
default term
-types o 0
- sequence,seqobj,seqcont,sequ,sobj 0
-arities o :: logic
+
+types
+ o sequence seqobj seqcont sequ sobj
+
+arities
+ o :: logic
+
consts
True,False :: "o"
"=" :: "['a,'a] => o" (infixl 50)
--- a/src/LK/lk.thy Thu Mar 17 13:54:50 1994 +0100
+++ b/src/LK/lk.thy Thu Mar 17 17:48:37 1994 +0100
@@ -7,11 +7,17 @@
*)
LK = Pure +
+
classes term < logic
+
default term
-types o 0
- sequence,seqobj,seqcont,sequ,sobj 0
-arities o :: logic
+
+types
+ o sequence seqobj seqcont sequ sobj
+
+arities
+ o :: logic
+
consts
True,False :: "o"
"=" :: "['a,'a] => o" (infixl 50)