src/HOL/HOL.thy
changeset 30980 fe0855471964
parent 30970 3fe2e418a071
child 31024 0fdf666e08bf
     1.1 --- a/src/HOL/HOL.thy	Sat Apr 25 20:31:27 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Apr 25 21:28:04 2009 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  imports Pure "~~/src/Tools/Code_Generator"
     1.5  uses
     1.6    ("Tools/hologic.ML")
     1.7 +  "~~/src/Tools/auto_solve.ML"
     1.8    "~~/src/Tools/IsaPlanner/zipper.ML"
     1.9    "~~/src/Tools/IsaPlanner/isand.ML"
    1.10    "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.11 @@ -1921,7 +1922,7 @@
    1.12  quickcheck_params [size = 5, iterations = 50]
    1.13  
    1.14  
    1.15 -subsection {* Nitpick hooks *}
    1.16 +subsection {* Nitpick setup *}
    1.17  
    1.18  text {* This will be relocated once Nitpick is moved to HOL. *}
    1.19  
    1.20 @@ -1947,10 +1948,14 @@
    1.21    val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    1.22  )
    1.23  *}
    1.24 -setup {* Nitpick_Const_Def_Thms.setup
    1.25 -         #> Nitpick_Const_Simp_Thms.setup
    1.26 -         #> Nitpick_Const_Psimp_Thms.setup
    1.27 -         #> Nitpick_Ind_Intro_Thms.setup *}
    1.28 +
    1.29 +setup {*
    1.30 +  Nitpick_Const_Def_Thms.setup
    1.31 +  #> Nitpick_Const_Simp_Thms.setup
    1.32 +  #> Nitpick_Const_Psimp_Thms.setup
    1.33 +  #> Nitpick_Ind_Intro_Thms.setup
    1.34 +*}
    1.35 +
    1.36  
    1.37  subsection {* Legacy tactics and ML bindings *}
    1.38