# HG changeset patch
# User wenzelm
# Date 966501349 -7200
# Node ID 3ade112482afdcc8452465dcc907d6704ef003dd
# Parent  d9aa8ca06bc2818c68f32b85b5f65575c489c5d1
renamed 'RS' to 'THEN';
'symmetric' attribute;

diff -r d9aa8ca06bc2 -r 3ade112482af src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Aug 17 10:34:52 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Aug 17 10:35:49 2000 +0200
@@ -79,7 +79,7 @@
   show "\<exists>y. (a, y) \<in> g" ..
   assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
   show "b = (SOME y. (a, y) \<in> g)"
-  proof (rule select_equality [RS sym])
+  proof (rule select_equality [symmetric])
     fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
   qed
 qed
diff -r d9aa8ca06bc2 -r 3ade112482af src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 17 10:34:52 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 17 10:35:49 2000 +0200
@@ -271,7 +271,7 @@
                   by (simp add: Let_def)
                 also have 
                   "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
-                  by (rule decomp_H'_H [RS sym]) (simp! add: x')+
+                  by (rule decomp_H'_H [symmetric]) (simp! add: x')+
                 also have 
                   "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
                     in h y + a * xi) = h' x" by (simp!)
@@ -328,7 +328,7 @@
 proof -
 assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
 "is_linearform F f"  "\<forall>x \<in> F. |f x| <= p x"
-have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
+have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [THEN iffD1])
 hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
           \<and> (\<forall>x \<in> E. g x <= p x)"
 by (simp! only: HahnBanach)
diff -r d9aa8ca06bc2 -r 3ade112482af src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 17 10:34:52 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 17 10:35:49 2000 +0200
@@ -185,9 +185,9 @@
       also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
         by simp;
       also; have "h y1 + a1 * xi = h' x1";
-        by (rule h'_definite [RS sym]);
+        by (rule h'_definite [symmetric]);
       also; have "h y2 + a2 * xi = h' x2"; 
-        by (rule h'_definite [RS sym]);
+        by (rule h'_definite [symmetric]);
       finally; show ?thesis; .;
     qed;
  
@@ -229,7 +229,7 @@
       also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
 	by (simp add: real_add_mult_distrib2 real_mult_assoc);
       also; have "h y1 + a1 * xi = h' x1"; 
-        by (rule h'_definite [RS sym]);
+        by (rule h'_definite [symmetric]);
       finally; show ?thesis; .;
     qed;
   qed;
@@ -300,7 +300,7 @@
       also; from nz vs y; have "... = p (y + a \<cdot> x0)";
         by (simp add: vs_add_mult_distrib1);
       also; from nz vs y; have "a * (h (rinv a \<cdot> y)) =  h y";
-        by (simp add: linearform_mult [RS sym]);
+        by (simp add: linearform_mult [symmetric]);
       finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
 
       hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y";
@@ -329,7 +329,7 @@
       also; from nz vs y; have "... = p (y + a \<cdot> x0)";
         by (simp add: vs_add_mult_distrib1);
       also; from nz vs y; have "a * h (rinv a \<cdot> y) = h y";
-        by (simp add: linearform_mult [RS sym]); 
+        by (simp add: linearform_mult [symmetric]); 
       finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
  
       hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)";
diff -r d9aa8ca06bc2 -r 3ade112482af src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 17 10:34:52 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 17 10:35:49 2000 +0200
@@ -333,7 +333,7 @@
       also assume "graph G g = x"
       also have "... \<in> c" .
       hence "x \<subseteq> \<Union>c" by fast
-      also have [RS sym]: "graph H h = \<Union>c" .
+      also have [symmetric]: "graph H h = \<Union>c" .
       finally show ?thesis .
     qed
   qed
@@ -476,7 +476,7 @@
     fix H' h' 
     assume "x \<in> H'" "graph H' h' \<subseteq> graph H h" 
       and a: "\<forall>x \<in> H'. h' x <= p x"
-    have [RS sym]: "h' x = h x" ..
+    have [symmetric]: "h' x = h x" ..
     also from a have "h' x <= p x " ..
     finally show ?thesis .  
   qed
@@ -522,7 +522,7 @@
       show "- p x <= h x"
       proof (rule real_minus_le)
 	from h have "- h x = h (- x)"
-          by (rule linearform_neg [RS sym])
+          by (rule linearform_neg [symmetric])
 	also from r have "... <= p (- x)" by (simp!)
 	also have "... = p x" 
         proof (rule seminorm_minus)
diff -r d9aa8ca06bc2 -r 3ade112482af src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 17 10:34:52 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 17 10:35:49 2000 +0200
@@ -227,7 +227,7 @@
   "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
     by (unfold vs_sum_def) fast
 
-lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
+lemmas vs_sumE = vs_sumD [THEN iffD1, elimify, standard]
 
 lemma vs_sumI [intro?]: 
   "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
@@ -343,7 +343,7 @@
   qed
 
   show "v1 = v2"
-  proof (rule vs_add_minus_eq [RS sym])
+  proof (rule vs_add_minus_eq [symmetric])
     show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
     show "v1 \<in> E" ..
     show "v2 \<in> E" ..
@@ -372,7 +372,7 @@
     show "H \<inter> (lin x') = {0}" 
     proof
       show "H \<inter> lin x' <= {0}" 
-      proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2])
+      proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2])
         fix x assume "x \<in> H" "x \<in> lin x'" 
         thus "x = 0"
         proof (unfold lin_def, elim CollectE exE conjE)
@@ -406,7 +406,7 @@
   from c show "y1 = y2" by simp
   
   show  "a1 = a2" 
-  proof (rule vs_mult_right_cancel [RS iffD1])
+  proof (rule vs_mult_right_cancel [THEN iffD1])
     from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
   qed
 qed
diff -r d9aa8ca06bc2 -r 3ade112482af src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Aug 17 10:34:52 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Aug 17 10:35:49 2000 +0200
@@ -292,11 +292,11 @@
 
 lemma vs_add_minus_cancel [simp]:  
   "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y" 
-  by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
+  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 
 
 lemma vs_minus_add_cancel [simp]: 
   "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y" 
-  by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
+  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 
 
 lemma vs_minus_add_distrib [simp]:  
   "[| is_vectorspace V; x \<in> V; y \<in> V |] 
@@ -323,7 +323,7 @@
     by (simp! only: vs_add_assoc vs_neg_closed)
   also assume "x + y = x + z"
   also have "- x + (x + z) = - x + x + z" 
-    by (simp! only: vs_add_assoc [RS sym] vs_neg_closed)
+    by (simp! only: vs_add_assoc [symmetric] vs_neg_closed)
   also have "... = z" by (simp!)
   finally show ?R .
 qed force
@@ -336,7 +336,7 @@
 lemma vs_add_assoc_cong: 
   "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |] 
   ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
-  by (simp only: vs_add_assoc [RS sym]) 
+  by (simp only: vs_add_assoc [symmetric]) 
 
 lemma vs_mult_left_commute: 
   "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
@@ -504,7 +504,7 @@
   proof
     assume l: ?L
     have "x + z = 0" 
-    proof (rule vs_add_left_cancel [RS iffD1])
+    proof (rule vs_add_left_cancel [THEN iffD1])
       have "y + (x + z) = x + (y + z)" by (simp!)
       also note l
       also have "y = y + 0" by (simp!)