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"]);