changeset 62390 | 842917225d56 |
parent 61990 | 39e4a93ad36e |
child 63167 | 0909deb8059b |
--- a/src/HOL/NanoJava/TypeRel.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/NanoJava/TypeRel.thy Tue Feb 23 16:25:08 2016 +0100 @@ -47,7 +47,7 @@ "subcls1 = (SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" apply (unfold subcls1_def is_class_def) -apply (auto split:split_if_asm) +apply (auto split:if_split_asm) done lemma finite_subcls1: "finite subcls1"