src/HOL/Bali/DeclConcepts.thy
changeset 24038 18182c4aec9e
parent 23747 b07cff284683
child 25143 2a1acc88a180
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sun Jul 29 14:29:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sun Jul 29 14:29:52 2007 +0200
     1.3 @@ -1553,7 +1553,7 @@
     1.4    (\<exists>i. iface G (decliface m) = Some i \<and> 
     1.5    table_of (imethods i) sig = Some (mthd m)) \<and>  
     1.6    (I,decliface m) \<in> (subint1 G)^* \<and> m \<in> imethds G (decliface m) sig"
     1.7 -apply (erule make_imp)
     1.8 +apply (erule rev_mp)
     1.9  apply (rule ws_subint1_induct, assumption, assumption)
    1.10  apply (subst imethds_rec, erule conjunct1, assumption)
    1.11  apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
    1.12 @@ -1617,7 +1617,7 @@
    1.13  "\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> \<Longrightarrow>
    1.14   (\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and> 
    1.15   G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m"   
    1.16 -apply (erule make_imp)
    1.17 +apply (erule rev_mp)
    1.18  apply (rule ws_subcls1_induct, assumption, assumption)
    1.19  apply (subst methd_rec, assumption)
    1.20  apply (case_tac "Ca=Object")
    1.21 @@ -2176,7 +2176,7 @@
    1.22    (\<exists>d. class G (declclassf efn) = Some d \<and> 
    1.23                      table_of (cfields d) (fname efn)=Some f) \<and> 
    1.24    G\<turnstile>C \<preceq>\<^sub>C (declclassf efn)  \<and> table_of (fields G (declclassf efn)) efn = Some f"
    1.25 -apply (erule make_imp)
    1.26 +apply (erule rev_mp)
    1.27  apply (rule ws_subcls1_induct, assumption, assumption)
    1.28  apply (subst fields_rec, assumption)
    1.29  apply clarify
    1.30 @@ -2207,7 +2207,7 @@
    1.31  lemma fields_mono_lemma: 
    1.32  "\<lbrakk>x \<in> set (fields G C); G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> 
    1.33   \<Longrightarrow> x \<in> set (fields G D)"
    1.34 -apply (erule make_imp)
    1.35 +apply (erule rev_mp)
    1.36  apply (erule converse_rtrancl_induct)
    1.37  apply  fast
    1.38  apply (drule subcls1D)