# HG changeset patch
# User wenzelm
# Date 1318452503 -7200
# Node ID 2214ba5bdfff1082a7438af526f30f3887c446c4
# Parent  09de0d0de645a05172a25b6f8223ce632e39101b
modernized structure Induct_Tacs;

diff -r 09de0d0de645 -r 2214ba5bdfff src/HOL/HOL.thy
--- 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 *}
diff -r 09de0d0de645 -r 2214ba5bdfff src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- 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 _ = 
diff -r 09de0d0de645 -r 2214ba5bdfff src/HOL/MicroJava/J/JTypeSafe.thy
--- 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")
diff -r 09de0d0de645 -r 2214ba5bdfff src/HOL/Nominal/nominal_atoms.ML
--- 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
diff -r 09de0d0de645 -r 2214ba5bdfff src/HOL/TLA/Memory/MemoryImplementation.thy
--- 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);
diff -r 09de0d0de645 -r 2214ba5bdfff src/Tools/induct_tacs.ML
--- 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 *)