author paulson Thu Oct 17 10:56:00 2002 +0200 (2002-10-17) changeset 13652 172600c40793 parent 13651 ac80e101306a child 13653 ef123b9e8089
```     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.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
```