fixed unfold of facts;
authorwenzelm
Tue Sep 21 18:11:08 1999 +0200 (1999-09-21)
changeset 756762384a807775
parent 7566 c5a3f980a7af
child 7568 436c87ac2fac
fixed unfold of facts;
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/Subspace.thy
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 17:31:20 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 18:11:08 1999 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4      proof (intro isUbI setleI ballI);
     1.5        fix y; assume "y: B V norm f";
     1.6        thus le: "y <= c";
     1.7 -      proof (-, unfold B_def, elim CollectE disjE bexE);
     1.8 +      proof (unfold B_def, elim CollectE disjE bexE);
     1.9  	fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
    1.10  	assume x: "x : V";
    1.11          have lt: "0r < norm x";  by (simp! add: normed_vs_norm_gt_zero);
     2.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 17:31:20 1999 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 18:11:08 1999 +0200
     2.3 @@ -120,7 +120,7 @@
     2.4    proof (intro ballI);
     2.5      fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
     2.6      thus "x1 [+] x2 : lin x";
     2.7 -    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);   (* FIXME !? *)
     2.8 +    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
     2.9        fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
    2.10        show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
    2.11      qed;
    2.12 @@ -130,7 +130,7 @@
    2.13    proof (intro ballI allI);
    2.14      fix x1 a; assume "x1 : lin x"; 
    2.15      thus "a [*] x1 : lin x";
    2.16 -    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);
    2.17 +    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
    2.18        fix a1; assume "x1 = a1 [*] x";
    2.19        show "a [*] x1 = (a * a1) [*] x"; by (simp!);
    2.20      qed;
    2.21 @@ -257,7 +257,7 @@
    2.22      proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
    2.23        fix x; assume "x:H" "x:lin x0"; 
    2.24        thus "x = <0>";
    2.25 -      proof (-, unfold lin_def, elim CollectE exE);
    2.26 +      proof (unfold lin_def, elim CollectE exE);
    2.27          fix a; assume "x = a [*] x0";
    2.28          show ?thesis;
    2.29          proof (rule case [of "a = 0r"]);