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/Real/HahnBanach/HahnBanachExtLemmas.thy
changeset 9906 5c027cca6262
parent 9623 3ade112482af
child 10007 64bf7da1994a 
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -273,7 +273,7 @@
     by case analysis on $a$. *};
 
     also; have "... <= p (y + a \<cdot> x0)";
-    proof (rule linorder_less_split); 
+    proof (rule linorder_cases);
 
       assume z: "a = #0"; 
       with vs y a; show ?thesis; by simp;
isabelle