src/HOL/HOL.thy
changeset 45014 0e847655b2d8
parent 44921 58eef4843641
child 45133 2214ba5bdfff
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 20 01:32:04 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Sep 20 05:47:11 2011 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    ("Tools/simpdata.ML")
     1.5    "~~/src/Tools/atomize_elim.ML"
     1.6    "~~/src/Tools/induct.ML"
     1.7 +  ("~~/src/Tools/induction.ML")
     1.8    ("~~/src/Tools/induct_tacs.ML")
     1.9    ("Tools/recfun_codegen.ML")
    1.10    ("Tools/cnf_funcs.ML")
    1.11 @@ -1490,8 +1491,10 @@
    1.12  )
    1.13  *}
    1.14  
    1.15 +use "~~/src/Tools/induction.ML"
    1.16 +
    1.17  setup {*
    1.18 -  Induct.setup #>
    1.19 +  Induct.setup #> Induction.setup #>
    1.20    Context.theory_map (Induct.map_simpset (fn ss => ss
    1.21      setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
    1.22        map (Simplifier.rewrite_rule (map Thm.symmetric