# HG changeset patch
# User wenzelm
# Date 1213024028 -7200
# Node ID c1c27955d7ddd91cc798d02dfab7302ee6e72fd7
# Parent  2cf13a72e1704d0094d21e7dc68e7271a282ed31
adapted case_tac/induct_tac;

diff -r 2cf13a72e170 -r c1c27955d7dd src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Mon Jun 09 17:07:08 2008 +0200
@@ -1207,7 +1207,7 @@
 --{* 34 subgoals left *}
 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
-apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
+apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
 apply(simp_all add:Graph10)
 --{* 47 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
diff -r 2cf13a72e170 -r c1c27955d7dd src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon Jun 09 17:07:08 2008 +0200
@@ -196,7 +196,7 @@
 apply fastsimp
 --{* 5 subgoals left *}
 prefer 5
-apply(tactic {* ALLGOALS (case_tac "j=k") *})
+apply(case_tac [!] "j=k")
 --{* 10 subgoals left *}
 apply simp_all
 apply(erule_tac x=k in allE)
@@ -502,8 +502,8 @@
 
 lemma Example2_lemma2_aux2: 
   "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
-apply(induct j)
- apply (simp_all cong:setsum_cong)
+apply(induct j) 
+ apply simp_all
 done
 
 lemma Example2_lemma2: 
diff -r 2cf13a72e170 -r c1c27955d7dd src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Jun 09 17:07:08 2008 +0200
@@ -94,7 +94,7 @@
               val stmnt2 = HOLogic.mk_Trueprop
                   (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
-              val proof2 = fn _ => EVERY [case_tac "y" 1,
+              val proof2 = fn _ => EVERY [DatatypePackage.case_tac "y" 1,
                                           asm_simp_tac (HOL_basic_ss addsimps simp1) 1,
                                           rtac @{thm exI} 1,
                                           rtac @{thm refl} 1]
diff -r 2cf13a72e170 -r c1c27955d7dd src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Jun 09 17:07:08 2008 +0200
@@ -96,7 +96,7 @@
   in pg'' thy defs t tacs end;
 
 fun case_UU_tac rews i v =
-  case_tac (v^"=UU") i THEN
+  DatatypePackage.case_tac (v^"=UU") i THEN
   asm_simp_tac (HOLCF_ss addsimps rews) i;
 
 val chain_tac =
@@ -647,7 +647,7 @@
       fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
       val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
       val tacs = [
-        induct_tac "n" 1,
+        DatatypePackage.induct_tac "n" 1,
         simp_tac iterate_Cprod_ss 1,
         asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
     in pg copy_take_defs goal tacs end;
@@ -678,7 +678,7 @@
       fun eq_tacs ((dn, _), cons) = map con_tac cons;
       val tacs =
         simp_tac iterate_Cprod_ss 1 ::
-        induct_tac "n" 1 ::
+        DatatypePackage.induct_tac "n" 1 ::
         simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
         asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
         TRY (safe_tac HOL_cs) ::
@@ -750,7 +750,7 @@
           val tacs1 = [
             quant_tac 1,
             simp_tac HOL_ss 1,
-            induct_tac "n" 1,
+            DatatypePackage.induct_tac "n" 1,
             simp_tac (take_ss addsimps prems) 1,
             TRY (safe_tac HOL_cs)];
           fun arg_tac arg =
@@ -845,7 +845,7 @@
               maps con_tacs cons;
             val tacs =
               rtac allI 1 ::
-              induct_tac "n" 1 ::
+              DatatypePackage.induct_tac "n" 1 ::
               simp_tac take_ss 1 ::
               TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
               flat (mapn foo_tacs 1 (conss ~~ cases));
@@ -938,7 +938,7 @@
         REPEAT (CHANGED (asm_simp_tac take_ss 1))];
       val tacs = [
         rtac impI 1,
-        induct_tac "n" 1,
+        DatatypePackage.induct_tac "n" 1,
         simp_tac take_ss 1,
         safe_tac HOL_cs] @
         flat (mapn x_tacs 0 xs);