src/HOL/Hahn_Banach/Zorn_Lemma.thy
changeset 32960 69916a850301
parent 31795 be3e1cc5005c
child 44887 7ca82df6e951
     1.1 --- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -31,13 +31,13 @@
     1.4      proof cases
     1.5  
     1.6        txt {* If @{text c} is an empty chain, then every element in
     1.7 -	@{text S} is an upper bound of @{text c}. *}
     1.8 +        @{text S} is an upper bound of @{text c}. *}
     1.9  
    1.10        assume "c = {}"
    1.11        with aS show ?thesis by fast
    1.12  
    1.13        txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
    1.14 -	bound of @{text c}, lying in @{text S}. *}
    1.15 +        bound of @{text c}, lying in @{text S}. *}
    1.16  
    1.17      next
    1.18        assume "c \<noteq> {}"
    1.19 @@ -47,7 +47,7 @@
    1.20          show "\<Union>c \<in> S"
    1.21          proof (rule r)
    1.22            from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
    1.23 -	  show "c \<in> chain S" by fact
    1.24 +          show "c \<in> chain S" by fact
    1.25          qed
    1.26        qed
    1.27      qed