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