--- a/src/ZF/Zorn.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Zorn.thy Sat Dec 09 13:36:11 1995 +0100
@@ -14,10 +14,10 @@
Zorn = OrderArith + AC + Inductive +
consts
- Subset_rel :: "i=>i"
- increasing :: "i=>i"
- chain, maxchain :: "i=>i"
- super :: "[i,i]=>i"
+ Subset_rel :: i=>i
+ increasing :: i=>i
+ chain, maxchain :: i=>i
+ super :: [i,i]=>i
defs
Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
@@ -34,7 +34,7 @@
are therefore unconditional.
**)
consts
- "TFin" :: "[i,i]=>i"
+ "TFin" :: [i,i]=>i
inductive
domains "TFin(S,next)" <= "Pow(S)"