src/HOL/HOL.thy
changeset 45133 2214ba5bdfff
parent 45014 0e847655b2d8
child 45171 262f179665f9
     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 *}