src/FOL/IFOL.thy

   "~~/src/Tools/IsaPlanner/isand.ML"
   "~~/src/Tools/IsaPlanner/rw_tools.ML"
   "~~/src/Tools/IsaPlanner/rw_inst.ML"
   "~~/src/Tools/eqsubst.ML"
   "~~/src/Provers/quantifier1.ML"
+  "~~/src/Tools/intuitionistic.ML"
   "~~/src/Tools/project_rule.ML"
   "~~/src/Tools/atomize_elim.ML"
   ("fologic.ML")
   ("hypsubstdata.ML")
   ("intprover.ML")

 setup hypsubst_setup
 use "intprover.ML"
 
 
 subsection {* Intuitionistic Reasoning *}
+
+setup {* Intuitionistic.method_setup "iprover" *}
 
 lemma impE':
   assumes 1: "P --> Q"
     and 2: "Q ==> R"
     and 3: "P --> Q ==> P"