# HG changeset patch
# User wenzelm
# Date 1213108994 -7200
# Node ID 97e9dae572841123bde5f05add4706429190cc92
# Parent  56617a7b68c58c58b40890427e30d032e102dc91
case_split_tac (works without context);

diff -r 56617a7b68c5 -r 97e9dae57284 src/HOL/MicroJava/Comp/Index.thy
--- 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)
diff -r 56617a7b68c5 -r 97e9dae57284 src/HOL/Nominal/Examples/Class.thy
--- 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)
diff -r 56617a7b68c5 -r 97e9dae57284 src/HOL/TLA/Memory/MemoryImplementation.thy
--- 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