src/HOL/Sledgehammer.thy
changeset 35866 513074557e06
parent 35865 2f8fb5242799
child 35867 16279c4c7a33
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Mar 19 13:02:18 2010 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Mar 19 15:07:44 2010 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4    ("Tools/ATP_Manager/atp_manager.ML")
     1.5    ("Tools/ATP_Manager/atp_wrapper.ML")
     1.6    ("Tools/ATP_Manager/atp_minimal.ML")
     1.7 +  ("Tools/Sledgehammer/sledgehammer_isar.ML")
     1.8    ("Tools/Sledgehammer/meson_tactic.ML")
     1.9    ("Tools/Sledgehammer/metis_tactics.ML")
    1.10  begin
    1.11 @@ -90,6 +91,7 @@
    1.12  apply (simp add: COMBC_def) 
    1.13  done
    1.14  
    1.15 +
    1.16  subsection {* Setup of external ATPs *}
    1.17  
    1.18  use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    1.19 @@ -122,6 +124,8 @@
    1.20  setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
    1.21  setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
    1.22  
    1.23 +use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.24 +
    1.25  
    1.26  subsection {* The MESON prover *}
    1.27