--- a/src/HOL/MicroJava/Comp/Index.thy Tue Jun 10 16:43:07 2008 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy Tue Jun 10 16:43:14 2008 +0200
@@ -54,7 +54,7 @@
\<Longrightarrow> (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) =
the (loc x)"
apply (simp only: index_def gjmb_plns_def)
-apply (case_tac "(gmb G C S)")
+apply (case_tac "gmb G C S" rule: prod.exhaust)
apply (simp add: galldefs del: set_append map_append)
apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
apply (intro strip)
@@ -74,7 +74,7 @@
locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
apply (simp only: locvars_xstate_def locvars_locals_def index_def)
-apply (case_tac "(gmb G C S)", simp)
+apply (case_tac "gmb G C S" rule: prod.exhaust, simp)
apply (case_tac b, simp)
apply (rule conjI)
apply (simp add: gl_def)
--- a/src/HOL/Nominal/Examples/Class.thy Tue Jun 10 16:43:07 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Tue Jun 10 16:43:14 2008 +0200
@@ -16599,7 +16599,7 @@
\<Longrightarrow> P (x1,x2,x3)"
shows "P (x1,x2,x3)"
apply(rule_tac my_wf_induct_triple[OF a])
-apply(case_tac x)
+apply(case_tac x rule: prod.exhaust)
apply(simp)
apply(case_tac b)
apply(simp)
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Jun 10 16:43:07 2008 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Jun 10 16:43:14 2008 +0200
@@ -763,12 +763,11 @@
*)
ML {*
fun split_idle_tac ss simps i =
- EVERY [TRY (rtac @{thm actionI} i),
- DatatypePackage.case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
- rewrite_goals_tac @{thms action_rews},
- forward_tac [temp_use @{thm Step1_4_7}] i,
- asm_full_simp_tac (ss addsimps simps) i
- ]
+ TRY (rtac @{thm actionI} i) THEN
+ case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
+ rewrite_goals_tac @{thms action_rews} THEN
+ forward_tac [temp_use @{thm Step1_4_7}] i THEN
+ asm_full_simp_tac (ss addsimps simps) i
*}
(* ----------------------------------------------------------------------
Combine steps 1.2 and 1.4 to prove that the implementation satisfies