equal
deleted
inserted
replaced
121 apply (unfold wf_syscls_def class_def) |
121 apply (unfold wf_syscls_def class_def) |
122 apply (auto simp: map_of_SomeI) |
122 apply (auto simp: map_of_SomeI) |
123 done |
123 done |
124 |
124 |
125 lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object" |
125 lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object" |
126 by (simp add: is_class_def not_None_eq) |
126 by (simp add: is_class_def) |
127 |
127 |
128 lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)" |
128 lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)" |
129 apply (simp add: ws_prog_def wf_syscls_def) |
129 apply (simp add: ws_prog_def wf_syscls_def) |
130 apply (simp add: is_class_def class_def) |
130 apply (simp add: is_class_def class_def) |
131 apply clarify |
131 apply clarify |