Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hahn_Banach/Zorn_Lemma.thy
changeset 81464 2575f1bd226b
parent 61879 e4f9d8f094fe 
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Nov 16 20:22:26 2024 +0100
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Nov 16 21:36:34 2024 +0100
@@ -27,17 +27,15 @@
   proof
     fix c assume "c \<in> chains S"
     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
-    proof cases
+    proof (cases "c = {}")
       txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper
         bound of \<open>c\<close>.\<close>
-
-      assume "c = {}"
+      case True
       with aS show ?thesis by fast
-
+    next
       txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in
         \<open>S\<close>.\<close>
-    next
-      assume "c \<noteq> {}"
+      case False
       show ?thesis
       proof
         show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
isabelle