src/HOL/Real/HahnBanach/Subspace.thy
 changeset 7567 62384a807775 parent 7566 c5a3f980a7af child 7656 2f18c0ffc348
```     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 17:31:20 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 18:11:08 1999 +0200
1.3 @@ -120,7 +120,7 @@
1.4    proof (intro ballI);
1.5      fix x1 x2; assume "x1 : lin x" "x2 : lin x";
1.6      thus "x1 [+] x2 : lin x";
1.7 -    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);   (* FIXME !? *)
1.8 +    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
1.9        fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
1.10        show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
1.11      qed;
1.12 @@ -130,7 +130,7 @@
1.13    proof (intro ballI allI);
1.14      fix x1 a; assume "x1 : lin x";
1.15      thus "a [*] x1 : lin x";
1.16 -    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);
1.17 +    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
1.18        fix a1; assume "x1 = a1 [*] x";
1.19        show "a [*] x1 = (a * a1) [*] x"; by (simp!);
1.20      qed;
1.21 @@ -257,7 +257,7 @@
1.22      proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
1.23        fix x; assume "x:H" "x:lin x0";
1.24        thus "x = <0>";
1.25 -      proof (-, unfold lin_def, elim CollectE exE);
1.26 +      proof (unfold lin_def, elim CollectE exE);
1.27          fix a; assume "x = a [*] x0";
1.28          show ?thesis;
1.29          proof (rule case [of "a = 0r"]);
```