# HG changeset patch
# User wenzelm
# Date 951252574 -3600
# Node ID 259073d16f84a2a7fe19302b78359857748c0ecc
# Parent  3453f73fad71260febc68d70194e10c6b24643fe
"cases" method;

diff -r 3453f73fad71 -r 259073d16f84 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Feb 22 21:48:50 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Feb 22 21:49:34 2000 +0100
@@ -253,7 +253,7 @@
  txt{* The proof is by case analysis on $x$. *};
  
   show ?thesis;
-  proof (rule case_split);
+  proof cases;
 
     txt {* For the case $x = \zero$ the thesis follows
     from the linearity of $f$: for every linear function
diff -r 3453f73fad71 -r 259073d16f84 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:48:50 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:49:34 2000 +0100
@@ -378,7 +378,7 @@
         proof (unfold lin_def, elim CollectE exE conjE);
           fix a; assume "x = a <*> x0";
           show ?thesis;
-          proof (rule case_split);
+          proof cases;
             assume "a = 0r"; show ?thesis; by (simp!);
           next;
             assume "a ~= 0r"; 
@@ -435,27 +435,27 @@
 $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
 
 lemma h0_definite:
-  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
                 in (h y) + a * xi);
   x = y + a <*> x0; is_vectorspace E; is_subspace H E;
   y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   ==> h0 x = h y + a * xi";
 proof -;  
   assume 
-    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
                in (h y) + a * xi)"
     "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
     "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   have "x : H + (lin x0)"; 
     by (simp! add: vs_sum_def lin_def) force+;
-  have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
+  have "EX! xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
   proof;
-    show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
+    show "EX xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
       by (force!);
   next;
     fix xa ya;
-    assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
-           "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
+    assume "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
+           "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
     show "xa = ya"; ;
     proof -;
       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
diff -r 3453f73fad71 -r 259073d16f84 src/HOL/Real/HahnBanach/ZornLemma.thy
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Tue Feb 22 21:48:50 2000 +0100
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Tue Feb 22 21:49:34 2000 +0100
@@ -27,7 +27,7 @@
   proof;
     fix c; assume "c:chain S"; 
     show "EX y:S. ALL z:c. z <= y";
-    proof (rule case_split);
+    proof cases;
  
       txt{* If $c$ is an empty chain, then every element
       in $S$ is an upper bound of $c$. *};