bug-fix with new records
authorschirmer
Thu Sep 30 05:08:17 2004 +0200 (2004-09-30)
changeset 1521715fa818ef624
parent 15216 2fac1f11b7f6
child 15218 39747a9e3c37
bug-fix with new records
src/HOL/Bali/TypeSafe.thy
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed Sep 29 22:40:40 2004 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu Sep 30 05:08:17 2004 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4    (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
     1.5  apply (unfold init_obj_def)
     1.6  apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
     1.7 -            simp add: obj.update_defs)
     1.8 +            )
     1.9  done
    1.10  
    1.11  lemma conforms_init_class_obj: