# HG changeset patch
# User wenzelm
# Date 1185712192 -7200
# Node ID 18182c4aec9e22bd603e17d1af6fe147b9594934
# Parent  0a41d2ebc0cdf4da0004d861a6ecfa21372d98c7
replaced make_imp by rev_mp;

diff -r 0a41d2ebc0cd -r 18182c4aec9e src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sun Jul 29 14:29:51 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy	Sun Jul 29 14:29:52 2007 +0200
@@ -959,7 +959,7 @@
     G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 
        G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
 apply (frule (1) finite_subset)
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (erule thin_rl)
 apply (erule finite_induct)
 apply  (unfold mtriples_def)
@@ -984,7 +984,7 @@
   ((\<forall>(C,sig)\<in>F. G,(A::'a triple set)\<turnstile>(f C sig::'a triple)) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>(g C sig::'a triple))) \<longrightarrow>  
       G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
 apply (frule (1) finite_subset)
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (erule thin_rl)
 apply (erule finite_induct)
 apply  clarsimp+
diff -r 0a41d2ebc0cd -r 18182c4aec9e src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Sun Jul 29 14:29:51 2007 +0200
+++ b/src/HOL/Bali/Basis.thy	Sun Jul 29 14:29:52 2007 +0200
@@ -21,11 +21,6 @@
 declare if_weak_cong [cong del] option.weak_case_cong [cong del]
 declare length_Suc_conv [iff]
 
-(*###to be phased out *)
-ML {*
-bind_thm ("make_imp", rearrange_prems [1,0] mp)
-*}
-
 lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
 apply auto
 done
diff -r 0a41d2ebc0cd -r 18182c4aec9e src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Sun Jul 29 14:29:51 2007 +0200
+++ b/src/HOL/Bali/Decl.thy	Sun Jul 29 14:29:52 2007 +0200
@@ -633,7 +633,7 @@
  "\<lbrakk>is_iface G I; ws_prog G; \<And>I i. \<lbrakk>iface G I = Some i \<and> 
    (\<forall>J \<in> set (isuperIfs i). (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J)\<rbrakk> \<Longrightarrow> P I
   \<rbrakk> \<Longrightarrow> P I"
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (rule subint1_induct)
 apply  assumption
 apply (simp (no_asm)) 
@@ -647,7 +647,7 @@
  (C \<noteq> Object \<longrightarrow> (C,(super c))\<in>subcls1 G \<and> 
                   P (super c) \<and> is_class G (super c))\<rbrakk> \<Longrightarrow> P C
  \<rbrakk> \<Longrightarrow> P C"
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (rule subcls1_induct)
 apply  assumption
 apply (simp (no_asm)) 
diff -r 0a41d2ebc0cd -r 18182c4aec9e src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Sun Jul 29 14:29:51 2007 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Sun Jul 29 14:29:52 2007 +0200
@@ -1553,7 +1553,7 @@
   (\<exists>i. iface G (decliface m) = Some i \<and> 
   table_of (imethods i) sig = Some (mthd m)) \<and>  
   (I,decliface m) \<in> (subint1 G)^* \<and> m \<in> imethds G (decliface m) sig"
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (rule ws_subint1_induct, assumption, assumption)
 apply (subst imethds_rec, erule conjunct1, assumption)
 apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
@@ -1617,7 +1617,7 @@
 "\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> \<Longrightarrow>
  (\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and> 
  G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m"   
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (rule ws_subcls1_induct, assumption, assumption)
 apply (subst methd_rec, assumption)
 apply (case_tac "Ca=Object")
@@ -2176,7 +2176,7 @@
   (\<exists>d. class G (declclassf efn) = Some d \<and> 
                     table_of (cfields d) (fname efn)=Some f) \<and> 
   G\<turnstile>C \<preceq>\<^sub>C (declclassf efn)  \<and> table_of (fields G (declclassf efn)) efn = Some f"
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (rule ws_subcls1_induct, assumption, assumption)
 apply (subst fields_rec, assumption)
 apply clarify
@@ -2207,7 +2207,7 @@
 lemma fields_mono_lemma: 
 "\<lbrakk>x \<in> set (fields G C); G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> 
  \<Longrightarrow> x \<in> set (fields G D)"
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (erule converse_rtrancl_induct)
 apply  fast
 apply (drule subcls1D)
diff -r 0a41d2ebc0cd -r 18182c4aec9e src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Sun Jul 29 14:29:51 2007 +0200
+++ b/src/HOL/Bali/Table.thy	Sun Jul 29 14:29:52 2007 +0200
@@ -186,7 +186,7 @@
 section {* Misc. *}
 
 lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y"
-apply (erule make_imp)
+apply (erule rev_mp)
 apply (induct l)
 apply simp
 apply (simp (no_asm))
diff -r 0a41d2ebc0cd -r 18182c4aec9e src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Sun Jul 29 14:29:51 2007 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Sun Jul 29 14:29:52 2007 +0200
@@ -373,7 +373,7 @@
 done
 
 lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K"
-apply (erule make_imp, erule implmt.induct)
+apply (erule rev_mp, erule implmt.induct)
 apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)
 done