changeset 24038 | 18182c4aec9e |
parent 23747 | b07cff284683 |
child 24783 | 5a3e336a2e37 |
--- 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