--- 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+
--- 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
--- 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))
--- 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)
--- 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))
--- 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