equal
deleted
inserted
replaced
1016 |
1016 |
1017 lemma wf_cdecl_all_standard_classes: |
1017 lemma wf_cdecl_all_standard_classes: |
1018 "Ball (set standard_classes) (wf_cdecl tprg)" |
1018 "Ball (set standard_classes) (wf_cdecl tprg)" |
1019 apply (unfold standard_classes_def Let_def |
1019 apply (unfold standard_classes_def Let_def |
1020 ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def) |
1020 ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def) |
1021 apply (simp (no_asm) add: wf_cdecl_def ws_cdecls) |
1021 apply (simp (no_asm) add: wf_cdecl_def ws_cdecls not_Some_eq) |
1022 apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def |
1022 apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def |
1023 intro: da.Skip) |
1023 intro: da.Skip) |
1024 apply (auto simp add: Object_def Classes_def standard_classes_def |
1024 apply (auto simp add: Object_def Classes_def standard_classes_def |
1025 SXcptC_def SXcpt_def) |
1025 SXcptC_def SXcpt_def) |
1026 done |
1026 done |