# HG changeset patch
# User wenzelm
# Date 937930268 -7200
# Node ID 62384a80777548439617e9a4b1e192c9f67f3b0f
# Parent  c5a3f980a7afae8b0a2a0eabdcdf48609af57c8d
fixed unfold of facts;

diff -r c5a3f980a7af -r 62384a807775 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- 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);
diff -r c5a3f980a7af -r 62384a807775 src/HOL/Real/HahnBanach/Subspace.thy
--- 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"]);