src/HOL/Real/HahnBanach/Subspace.thy
 changeset 8280 259073d16f84 parent 8203 2fcc6017cb72 child 8703 816d8f6513be
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:48:50 2000 +0100
1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:49:34 2000 +0100
1.3 @@ -378,7 +378,7 @@
1.4          proof (unfold lin_def, elim CollectE exE conjE);
1.5            fix a; assume "x = a <*> x0";
1.6            show ?thesis;
1.7 -          proof (rule case_split);
1.8 +          proof cases;
1.9              assume "a = 0r"; show ?thesis; by (simp!);
1.10            next;
1.11              assume "a ~= 0r";
1.12 @@ -435,27 +435,27 @@
1.13  $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
1.14
1.15  lemma h0_definite:
1.16 -  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.17 +  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.18                  in (h y) + a * xi);
1.19    x = y + a <*> x0; is_vectorspace E; is_subspace H E;
1.20    y:H; x0 ~: H; x0:E; x0 ~= <0> |]
1.21    ==> h0 x = h y + a * xi";
1.22  proof -;
1.23    assume
1.24 -    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.25 +    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.26                 in (h y) + a * xi)"
1.27      "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
1.28      "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
1.29    have "x : H + (lin x0)";
1.30      by (simp! add: vs_sum_def lin_def) force+;
1.31 -  have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
1.32 +  have "EX! xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
1.33    proof;
1.34 -    show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
1.35 +    show "EX xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
1.36        by (force!);
1.37    next;
1.38      fix xa ya;
1.39 -    assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
1.40 -           "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
1.41 +    assume "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
1.42 +           "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
1.43      show "xa = ya"; ;
1.44      proof -;
1.45        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";