| changeset 31166 | a90fe83f58ea |
| parent 28524 | 644b62cf678f |
| child 35102 | cc7a0b9f938c |
--- a/src/HOL/NanoJava/TypeRel.thy Fri May 15 10:01:57 2009 +0200 +++ b/src/HOL/NanoJava/TypeRel.thy Sat May 16 11:28:02 2009 +0200 @@ -56,7 +56,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 +apply (auto split:split_if_asm) done lemma finite_subcls1: "finite subcls1"