--- 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
--- 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)
--- 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)";
--- 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)
--- 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
--- 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!)