src/HOL/Real/HahnBanach/FunctionNorm.thy
changeset 7567 62384a807775
parent 7566 c5a3f980a7af
child 7656 2f18c0ffc348
     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);