--- a/src/HOL/HOL.thy Wed Oct 12 22:21:38 2011 +0200
+++ b/src/HOL/HOL.thy Wed Oct 12 22:48:23 2011 +0200
@@ -1574,7 +1574,7 @@
hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
use "~~/src/Tools/induct_tacs.ML"
-setup InductTacs.setup
+setup Induct_Tacs.setup
subsubsection {* Coherent logic *}
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Oct 12 22:21:38 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Oct 12 22:48:23 2011 +0200
@@ -174,7 +174,7 @@
val tacs1 = [
quant_tac ctxt 1,
simp_tac HOL_ss 1,
- InductTacs.induct_tac ctxt [[SOME "n"]] 1,
+ Induct_Tacs.induct_tac ctxt [[SOME "n"]] 1,
simp_tac (take_ss addsimps prems) 1,
TRY (safe_tac (put_claset HOL_cs ctxt))]
fun con_tac _ =
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Oct 12 22:21:38 2011 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Oct 12 22:48:23 2011 +0200
@@ -243,7 +243,7 @@
THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
-- "for if"
-apply( tactic {* (InductTacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
+apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
(asm_full_simp_tac @{simpset})) 7*})
apply (tactic "forward_hyp_tac")
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Oct 12 22:21:38 2011 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Oct 12 22:48:23 2011 +0200
@@ -132,7 +132,7 @@
(HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
val proof2 = fn {prems, context} =>
- InductTacs.case_tac context "y" 1 THEN
+ Induct_Tacs.case_tac context "y" 1 THEN
asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN
rtac @{thm exI} 1 THEN
rtac @{thm refl} 1
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Oct 12 22:21:38 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Oct 12 22:48:23 2011 +0200
@@ -794,7 +794,7 @@
fun split_idle_tac ctxt =
SELECT_GOAL
(TRY (rtac @{thm actionI} 1) THEN
- InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
+ Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
rewrite_goals_tac @{thms action_rews} THEN
forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
asm_full_simp_tac (simpset_of ctxt) 1);
--- a/src/Tools/induct_tacs.ML Wed Oct 12 22:21:38 2011 +0200
+++ b/src/Tools/induct_tacs.ML Wed Oct 12 22:48:23 2011 +0200
@@ -13,7 +13,7 @@
val setup: theory -> theory
end
-structure InductTacs: INDUCT_TACS =
+structure Induct_Tacs: INDUCT_TACS =
struct
(* case analysis *)