1.1 --- a/src/HOL/HOL.thy	Wed Oct 12 22:21:38 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Oct 12 22:48:23 2011 +0200
     1.3 @@ -1574,7 +1574,7 @@
     1.4  hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
     1.5  
     1.6  use "~~/src/Tools/induct_tacs.ML"
     1.7 -setup InductTacs.setup
     1.8 +setup Induct_Tacs.setup
     1.9  
    1.10  
    1.11  subsubsection {* Coherent logic *}

     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Oct 12 22:21:38 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Oct 12 22:48:23 2011 +0200
     2.3 @@ -174,7 +174,7 @@
     2.4            val tacs1 = [
     2.5              quant_tac ctxt 1,
     2.6              simp_tac HOL_ss 1,
     2.7 -            InductTacs.induct_tac ctxt [[SOME "n"]] 1,
     2.8 +            Induct_Tacs.induct_tac ctxt [[SOME "n"]] 1,
     2.9              simp_tac (take_ss addsimps prems) 1,
    2.10              TRY (safe_tac (put_claset HOL_cs ctxt))]
    2.11            fun con_tac _ = 

     3.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 12 22:21:38 2011 +0200
     3.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 12 22:48:23 2011 +0200
     3.3 @@ -243,7 +243,7 @@
     3.4         THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
     3.5  
     3.6  -- "for if"
     3.7 -apply( tactic {* (InductTacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
     3.8 +apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
     3.9    (asm_full_simp_tac @{simpset})) 7*})
    3.10  
    3.11  apply (tactic "forward_hyp_tac")

     4.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Oct 12 22:21:38 2011 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Oct 12 22:48:23 2011 +0200
     4.3 @@ -132,7 +132,7 @@
     4.4                    (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
     4.5  
     4.6                val proof2 = fn {prems, context} =>
     4.7 -                InductTacs.case_tac context "y" 1 THEN
     4.8 +                Induct_Tacs.case_tac context "y" 1 THEN
     4.9                  asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN
    4.10                  rtac @{thm exI} 1 THEN
    4.11                  rtac @{thm refl} 1

     5.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Oct 12 22:21:38 2011 +0200
     5.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Oct 12 22:48:23 2011 +0200
     5.3 @@ -794,7 +794,7 @@
     5.4  fun split_idle_tac ctxt =
     5.5    SELECT_GOAL
     5.6     (TRY (rtac @{thm actionI} 1) THEN
     5.7 -    InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
     5.8 +    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
     5.9      rewrite_goals_tac @{thms action_rews} THEN
    5.10      forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
    5.11      asm_full_simp_tac (simpset_of ctxt) 1);

     6.1 --- a/src/Tools/induct_tacs.ML	Wed Oct 12 22:21:38 2011 +0200
     6.2 +++ b/src/Tools/induct_tacs.ML	Wed Oct 12 22:48:23 2011 +0200
     6.3 @@ -13,7 +13,7 @@
     6.4    val setup: theory -> theory
     6.5  end
     6.6  
     6.7 -structure InductTacs: INDUCT_TACS =
     6.8 +structure Induct_Tacs: INDUCT_TACS =
     6.9  struct
    6.10  
    6.11  (* case analysis *)