src/HOL/HOL.thy

 
 theory HOL
 imports Pure "~~/src/Tools/Code_Generator"
 uses
   ("Tools/hologic.ML")
+  "~~/src/Tools/auto_solve.ML"
   "~~/src/Tools/IsaPlanner/zipper.ML"
   "~~/src/Tools/IsaPlanner/isand.ML"
   "~~/src/Tools/IsaPlanner/rw_tools.ML"
   "~~/src/Tools/IsaPlanner/rw_inst.ML"
   "~~/src/Tools/intuitionistic.ML"

 *}
 
 quickcheck_params [size = 5, iterations = 50]
 
 
-subsection {* Nitpick hooks *}
+subsection {* Nitpick setup *}
 
 text {* This will be relocated once Nitpick is moved to HOL. *}
 
 ML {*
 structure Nitpick_Const_Def_Thms = NamedThmsFun

 (
   val name = "nitpick_ind_intro"
   val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
 )
 *}
-setup {* Nitpick_Const_Def_Thms.setup
-         #> Nitpick_Const_Simp_Thms.setup
-         #> Nitpick_Const_Psimp_Thms.setup
-         #> Nitpick_Ind_Intro_Thms.setup *}
+
+setup {*
+  Nitpick_Const_Def_Thms.setup
+  #> Nitpick_Const_Simp_Thms.setup
+  #> Nitpick_Const_Psimp_Thms.setup
+  #> Nitpick_Ind_Intro_Thms.setup
+*}
+
 
 subsection {* Legacy tactics and ML bindings *}
 
 ML {*
 fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);