src/HOL/Library/Zorn.thy
changeset 23755 1c4672d130b1
parent 21404 eb85850d3eb7
child 25594 43c718438f9f
     1.1 --- a/src/HOL/Library/Zorn.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -33,12 +33,12 @@
     1.4      (if c \<notin> chain S | c \<in> maxchain S
     1.5      then c else SOME c'. c' \<in> super S c)"
     1.6  
     1.7 -consts
     1.8 +inductive_set
     1.9    TFin :: "'a set set => 'a set set set"
    1.10 -inductive "TFin S"
    1.11 -  intros
    1.12 +  for S :: "'a set set"
    1.13 +  where
    1.14      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    1.15 -    Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    1.16 +  | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    1.17    monos          Pow_mono
    1.18  
    1.19