src/HOL/Bali/Eval.thy

 apply  simp_all
 apply (case_tac "T")
 defer 
 apply (case_tac "a' = Null")
 apply  simp_all
+apply rules
 done
 
 constdefs
   catch ::"prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool"      ("_,_\<turnstile>catch _"[61,61,61]60)
  "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 

 by (auto elim: eval.Body)
 
 lemma unique_eval [rule_format (no_asm)]: 
   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
 apply (case_tac "ws")
-apply (simp only:)
-apply (erule thin_rl)
+apply hypsubst
 apply (erule eval_induct)
 apply (tactic {* ALLGOALS (EVERY'
       [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
 (* 31 subgoals *)
 prefer 28 (* Try *)