| changeset 18576 | 8d98b7711e47 |
| parent 18447 | da548623916a |
| child 22271 | 51a80e238b29 |
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/MicroJava/J/WellForm.thy Wed Jan 04 19:22:53 2006 +0100 @@ -123,7 +123,7 @@ done lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object" - by (simp add: is_class_def not_None_eq) + by (simp add: is_class_def) lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)" apply (simp add: ws_prog_def wf_syscls_def)