fixed comments and types
authorpaulson
Thu Oct 17 10:56:00 2002 +0200 (2002-10-17)
changeset 13652172600c40793
parent 13651 ac80e101306a
child 13653 ef123b9e8089
fixed comments and types
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Zorn.thy	Thu Oct 17 10:54:11 2002 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Thu Oct 17 10:56:00 2002 +0200
     1.3 @@ -1,8 +1,7 @@
     1.4 -(*  Title       \<in> Zorn.thy
     1.5 -    ID          \<in> $Id$
     1.6 -    Author      \<in> Jacques D. Fleuriot
     1.7 -    Copyright   \<in> 1998  University of Cambridge
     1.8 -    Description \<in> Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
     1.9 +(*  Title       : Zorn.thy
    1.10 +    ID          : $Id$
    1.11 +    Author      : Jacques D. Fleuriot
    1.12 +    Description : Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
    1.13  *) 
    1.14  
    1.15  header {*Zorn's Lemma*}
    1.16 @@ -14,21 +13,21 @@
    1.17  Abrial and Laffitte.  *}
    1.18  
    1.19  constdefs
    1.20 -  chain     ::  "'a::ord set => 'a set set"
    1.21 +  chain     ::  "'a set set => 'a set set set"
    1.22      "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}" 
    1.23  
    1.24 -  super     ::  "['a::ord set,'a set] => 'a set set"
    1.25 +  super     ::  "['a set set,'a set set] => 'a set set set"
    1.26      "super S c == {d. d \<in> chain(S) & c < d}"
    1.27  
    1.28 -  maxchain  ::  "'a::ord set => 'a set set"
    1.29 +  maxchain  ::  "'a set set => 'a set set set"
    1.30      "maxchain S == {c. c \<in> chain S & super S c = {}}"
    1.31  
    1.32 -  succ      ::  "['a::ord set,'a set] => 'a set"
    1.33 +  succ      ::  "['a set set,'a set set] => 'a set set"
    1.34      "succ S c == if (c \<notin> chain S| c \<in> maxchain S) 
    1.35                   then c else (@c'. c': (super S c))" 
    1.36  
    1.37  consts 
    1.38 -  "TFin" ::  "'a::ord set => 'a set set"
    1.39 +  "TFin" ::  "'a set set => 'a set set set"
    1.40  
    1.41  inductive "TFin(S)"
    1.42    intros