| changeset 18447 | da548623916a |
| parent 16417 | 9bc16273c2d4 |
| child 21765 | 89275a3ed7be |
--- a/src/HOL/Bali/TypeRel.thy Tue Dec 20 22:06:00 2005 +0100 +++ b/src/HOL/Bali/TypeRel.thy Wed Dec 21 12:02:57 2005 +0100 @@ -393,7 +393,7 @@ lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C" apply (erule implmt.induct) -apply (blast dest: implmt1D subcls1D)+ +apply (auto dest: implmt1D subcls1D) done