src/HOL/NanoJava/TypeRel.thy
changeset 14171 0cab06e3bbd0
parent 14134 0fdf5708c7a8
child 14952 47455995693d
     1.1 --- a/src/HOL/NanoJava/TypeRel.thy	Wed Aug 27 18:22:34 2003 +0200
     1.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Thu Aug 28 01:56:40 2003 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  done
     1.5  
     1.6  lemma subcls1_def2: 
     1.7 -"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
     1.8 +"subcls1 = (\<Sigma> C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
     1.9  apply (unfold subcls1_def is_class_def)
    1.10  apply auto
    1.11  done