--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Mar 13 07:07:07 2014 +0100
@@ -1268,7 +1268,6 @@
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (rule exI)+
apply (simp add: wf_prog_ws_prog [THEN comp_method])
- apply auto
done
@@ -2517,16 +2516,13 @@
(start_ST, start_LT C pTs (length lvars))))
= (start_ST, inited_LT C pTs lvars)")
prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption
-apply (simp only:)
apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
(start_ST, inited_LT C pTs lvars)))
= (start_ST, inited_LT C pTs lvars)")
prefer 2 apply (erule conjE)+
apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+
apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
-apply (simp only:)
-apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
- apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
+ apply (simp (no_asm_simp) add: is_inited_LT_def)
(* Return *)