--- a/src/HOL/Bali/Eval.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/Eval.thy Mon Sep 30 16:14:02 2002 +0200
@@ -160,6 +160,7 @@
defer
apply (case_tac "a' = Null")
apply simp_all
+apply rules
done
constdefs
@@ -1203,8 +1204,7 @@
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")]) *})