reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
authorblanchet
Tue Oct 26 12:17:19 2010 +0200 (2010-10-26)
changeset 4017800152d17855b
parent 40166 d3bc972b7d9d
child 40179 7ecfa9beef91
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
src/HOL/ATP.thy
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/Plain.thy
src/HOL/Refute.thy
src/HOL/Sledgehammer.thy
     1.1 --- a/src/HOL/ATP.thy	Tue Oct 26 11:51:09 2010 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue Oct 26 12:17:19 2010 +0200
     1.3 @@ -6,11 +6,10 @@
     1.4  header {* Automatic Theorem Provers (ATPs) *}
     1.5  
     1.6  theory ATP
     1.7 -imports HOL
     1.8 -uses
     1.9 -  "Tools/ATP/atp_problem.ML"
    1.10 -  "Tools/ATP/atp_proof.ML"
    1.11 -  "Tools/ATP/atp_systems.ML"
    1.12 +imports Plain
    1.13 +uses "Tools/ATP/atp_problem.ML"
    1.14 +     "Tools/ATP/atp_proof.ML"
    1.15 +     "Tools/ATP/atp_systems.ML"
    1.16  begin
    1.17  
    1.18  setup ATP_Systems.setup
     2.1 --- a/src/HOL/IsaMakefile	Tue Oct 26 11:51:09 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Oct 26 12:17:19 2010 +0200
     2.3 @@ -144,7 +144,6 @@
     2.4  	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
     2.5  
     2.6  PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
     2.7 -  ATP.thy \
     2.8    Complete_Lattice.thy \
     2.9    Complete_Partial_Order.thy \
    2.10    Datatype.thy \
    2.11 @@ -170,7 +169,6 @@
    2.12    Rings.thy \
    2.13    SAT.thy \
    2.14    Set.thy \
    2.15 -  Sledgehammer.thy \
    2.16    Sum_Type.thy \
    2.17    Tools/abel_cancel.ML \
    2.18    Tools/arith_data.ML \
    2.19 @@ -239,6 +237,7 @@
    2.20  	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
    2.21  
    2.22  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
    2.23 +  ATP.thy \
    2.24    Big_Operators.thy \
    2.25    Code_Evaluation.thy \
    2.26    Code_Numeral.thy \
    2.27 @@ -269,6 +268,7 @@
    2.28    Refute.thy \
    2.29    Semiring_Normalization.thy \
    2.30    SetInterval.thy \
    2.31 +  Sledgehammer.thy \
    2.32    SMT.thy \
    2.33    String.thy \
    2.34    Typerep.thy \
     3.1 --- a/src/HOL/Main.thy	Tue Oct 26 11:51:09 2010 +0200
     3.2 +++ b/src/HOL/Main.thy	Tue Oct 26 12:17:19 2010 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  header {* Main HOL *}
     3.5  
     3.6  theory Main
     3.7 -imports Plain Record Predicate_Compile Nitpick SMT Quotient
     3.8 +imports Plain Record Predicate_Compile Nitpick SMT
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Plain.thy	Tue Oct 26 11:51:09 2010 +0200
     4.2 +++ b/src/HOL/Plain.thy	Tue Oct 26 12:17:19 2010 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  header {* Plain HOL *}
     4.5  
     4.6  theory Plain
     4.7 -imports Datatype FunDef Extraction Sledgehammer
     4.8 +imports Datatype FunDef Extraction Metis
     4.9  begin
    4.10  
    4.11  text {*
     5.1 --- a/src/HOL/Refute.thy	Tue Oct 26 11:51:09 2010 +0200
     5.2 +++ b/src/HOL/Refute.thy	Tue Oct 26 12:17:19 2010 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  header {* Refute *}
     5.5  
     5.6  theory Refute
     5.7 -imports Hilbert_Choice List
     5.8 +imports Hilbert_Choice List Sledgehammer
     5.9  uses "Tools/refute.ML"
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Sledgehammer.thy	Tue Oct 26 11:51:09 2010 +0200
     6.2 +++ b/src/HOL/Sledgehammer.thy	Tue Oct 26 12:17:19 2010 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  header {* Sledgehammer: Isabelle--ATP Linkup *}
     6.5  
     6.6  theory Sledgehammer
     6.7 -imports ATP Metis
     6.8 +imports ATP
     6.9  uses "Tools/Sledgehammer/sledgehammer_util.ML"
    6.10       "Tools/Sledgehammer/sledgehammer_filter.ML"
    6.11       "Tools/Sledgehammer/sledgehammer_atp_translate.ML"