--- a/src/HOL/MicroJava/J/WellForm.thy Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Dec 21 12:02:57 2005 +0100
@@ -123,9 +123,7 @@
done
lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
-apply (unfold is_class_def)
-apply (simp (no_asm_simp))
-done
+ by (simp add: is_class_def not_None_eq)
lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)"
apply (simp add: ws_prog_def wf_syscls_def)
@@ -213,7 +211,7 @@
apply( rule impI)
apply( case_tac "C = Object")
apply( fast)
-apply safe
+apply auto
apply( frule (1) class_wf) apply (erule conjE)+
apply (frule wf_cdecl_ws_cdecl)
apply( frule (1) wf_cdecl_supD)
@@ -263,7 +261,7 @@
apply( rule impI)
apply( case_tac "C = Object")
apply( fast)
-apply safe
+apply auto
apply( frule (1) class_wf_struct)
apply( frule (1) wf_cdecl_supD)