src/HOL/Real/HahnBanach/Subspace.thy
 changeset 9623 3ade112482af parent 9408 d3d56e1d2ec1 child 9906 5c027cca6262
```     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 17 10:34:52 2000 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 17 10:35:49 2000 +0200
1.3 @@ -227,7 +227,7 @@
1.4    "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
1.5      by (unfold vs_sum_def) fast
1.6
1.7 -lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
1.8 +lemmas vs_sumE = vs_sumD [THEN iffD1, elimify, standard]
1.9
1.10  lemma vs_sumI [intro?]:
1.11    "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
1.12 @@ -343,7 +343,7 @@
1.13    qed
1.14
1.15    show "v1 = v2"
1.16 -  proof (rule vs_add_minus_eq [RS sym])
1.17 +  proof (rule vs_add_minus_eq [symmetric])
1.18      show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
1.19      show "v1 \<in> E" ..
1.20      show "v2 \<in> E" ..
1.21 @@ -372,7 +372,7 @@
1.22      show "H \<inter> (lin x') = {0}"
1.23      proof
1.24        show "H \<inter> lin x' <= {0}"
1.25 -      proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2])
1.26 +      proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2])
1.27          fix x assume "x \<in> H" "x \<in> lin x'"
1.28          thus "x = 0"
1.29          proof (unfold lin_def, elim CollectE exE conjE)
1.30 @@ -406,7 +406,7 @@
1.31    from c show "y1 = y2" by simp
1.32
1.33    show  "a1 = a2"
1.34 -  proof (rule vs_mult_right_cancel [RS iffD1])
1.35 +  proof (rule vs_mult_right_cancel [THEN iffD1])
1.36      from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
1.37    qed
1.38  qed
```