author wenzelm Tue, 21 Sep 1999 18:11:08 +0200 changeset 7567 62384a807775 parent 7566 c5a3f980a7af child 7568 436c87ac2fac
fixed unfold of facts;
```--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 17:31:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 18:11:08 1999 +0200
@@ -204,7 +204,7 @@
proof (intro isUbI setleI ballI);
fix y; assume "y: B V norm f";
thus le: "y <= c";
-      proof (-, unfold B_def, elim CollectE disjE bexE);
+      proof (unfold B_def, elim CollectE disjE bexE);
fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
assume x: "x : V";
have lt: "0r < norm x";  by (simp! add: normed_vs_norm_gt_zero);```
```--- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 17:31:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 18:11:08 1999 +0200
@@ -120,7 +120,7 @@
proof (intro ballI);
fix x1 x2; assume "x1 : lin x" "x2 : lin x";
thus "x1 [+] x2 : lin x";
-    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);   (* FIXME !? *)
+    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
qed;
@@ -130,7 +130,7 @@
proof (intro ballI allI);
fix x1 a; assume "x1 : lin x";
thus "a [*] x1 : lin x";
-    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);
+    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
fix a1; assume "x1 = a1 [*] x";
show "a [*] x1 = (a * a1) [*] x"; by (simp!);
qed;
@@ -257,7 +257,7 @@
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
fix x; assume "x:H" "x:lin x0";
thus "x = <0>";
-      proof (-, unfold lin_def, elim CollectE exE);
+      proof (unfold lin_def, elim CollectE exE);
fix a; assume "x = a [*] x0";
show ?thesis;
proof (rule case [of "a = 0r"]);```