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
```