author | schirmer |
Thu, 30 Sep 2004 05:08:17 +0200 | |
changeset 15217 | 15fa818ef624 |
parent 15216 | 2fac1f11b7f6 |
child 15218 | 39747a9e3c37 |
--- a/src/HOL/Bali/TypeSafe.thy Wed Sep 29 22:40:40 2004 +0200 +++ b/src/HOL/Bali/TypeSafe.thy Thu Sep 30 05:08:17 2004 +0200 @@ -263,7 +263,7 @@ (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)" apply (unfold init_obj_def) apply (auto elim!: conforms_gupd dest!: oconf_init_obj - simp add: obj.update_defs) + ) done lemma conforms_init_class_obj: