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/ZF/Cardinal_AC.thy
changeset 67443 3abf6a722518
parent 61980 6b780867d426
child 69593 3dda49e08b9d 
--- a/src/ZF/Cardinal_AC.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/ZF/Cardinal_AC.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -222,7 +222,7 @@
   note lt_subset_trans [OF _ _ OU, trans]
   show ?thesis
     proof (cases "W=0")
-      case True  \<comment>\<open>solve the easy 0 case\<close>
+      case True  \<comment> \<open>solve the easy 0 case\<close>
       thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
     next
       case False
isabelle