src/HOL/Bali/Example.thy
changeset 18576 8d98b7711e47
parent 18551 be0705186ff5
child 20769 5d538d3d5e2a
     1.1 --- a/src/HOL/Bali/Example.thy	Wed Jan 04 17:04:11 2006 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Wed Jan 04 19:22:53 2006 +0100
     1.3 @@ -1018,7 +1018,7 @@
     1.4    "Ball (set standard_classes) (wf_cdecl tprg)"
     1.5  apply (unfold standard_classes_def Let_def 
     1.6         ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
     1.7 -apply (simp (no_asm) add: wf_cdecl_def ws_cdecls not_Some_eq)
     1.8 +apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
     1.9  apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def 
    1.10              intro: da.Skip)
    1.11  apply (auto simp add: Object_def Classes_def standard_classes_def