# HG changeset patch
# User paulson
# Date 1034844960 -7200
# Node ID 172600c4079305c590904fd99376b6e03cd7fb6b
# Parent  ac80e101306aa05edb002fa26c8d247c3462ab12
fixed comments and types

diff -r ac80e101306a -r 172600c40793 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Thu Oct 17 10:54:11 2002 +0200
+++ b/src/HOL/Library/Zorn.thy	Thu Oct 17 10:56:00 2002 +0200
@@ -1,8 +1,7 @@
-(*  Title       \<in> Zorn.thy
-    ID          \<in> $Id$
-    Author      \<in> Jacques D. Fleuriot
-    Copyright   \<in> 1998  University of Cambridge
-    Description \<in> Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
+(*  Title       : Zorn.thy
+    ID          : $Id$
+    Author      : Jacques D. Fleuriot
+    Description : Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
 *) 
 
 header {*Zorn's Lemma*}
@@ -14,21 +13,21 @@
 Abrial and Laffitte.  *}
 
 constdefs
-  chain     ::  "'a::ord set => 'a set set"
+  chain     ::  "'a set set => 'a set set set"
     "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}" 
 
-  super     ::  "['a::ord set,'a set] => 'a set set"
+  super     ::  "['a set set,'a set set] => 'a set set set"
     "super S c == {d. d \<in> chain(S) & c < d}"
 
-  maxchain  ::  "'a::ord set => 'a set set"
+  maxchain  ::  "'a set set => 'a set set set"
     "maxchain S == {c. c \<in> chain S & super S c = {}}"
 
-  succ      ::  "['a::ord set,'a set] => 'a set"
+  succ      ::  "['a set set,'a set set] => 'a set set"
     "succ S c == if (c \<notin> chain S| c \<in> maxchain S) 
                  then c else (@c'. c': (super S c))" 
 
 consts 
-  "TFin" ::  "'a::ord set => 'a set set"
+  "TFin" ::  "'a set set => 'a set set set"
 
 inductive "TFin(S)"
   intros