changeset 10612 | 779af7c58743 |
parent 10592 | fc0b575a2cf7 |
child 10630 | f89c3fc4fde1 |
--- a/src/HOL/MicroJava/BV/JType.thy Wed Dec 06 19:05:50 2000 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Wed Dec 06 19:09:34 2000 +0100 @@ -68,7 +68,7 @@ moreover from R wf ty have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis" - by (auto simp add: is_ty_def subcls1_def is_class_def class_def + by (auto simp add: is_ty_def subcls1_def elim: converse_rtranclE split: ref_ty.splits) ultimately