moved sledgehammer to Plain; tuned dependencies
authorhaftmann
Mon Oct 25 13:34:57 2010 +0200 (2010-10-25)
changeset 40121e7a80c6752c9
parent 40120 c57fffa2727c
child 40122 1d8ad2ff3e01
moved sledgehammer to Plain; tuned dependencies
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	Mon Oct 25 13:34:57 2010 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Oct 25 13:34:57 2010 +0200
     1.3 @@ -6,10 +6,11 @@
     1.4  header {* Automatic Theorem Provers (ATPs) *}
     1.5  
     1.6  theory ATP
     1.7 -imports Plain
     1.8 -uses "Tools/ATP/atp_problem.ML"
     1.9 -     "Tools/ATP/atp_proof.ML"
    1.10 -     "Tools/ATP/atp_systems.ML"
    1.11 +imports HOL
    1.12 +uses
    1.13 +  "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	Mon Oct 25 13:34:57 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Oct 25 13:34:57 2010 +0200
     2.3 @@ -144,6 +144,7 @@
     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 @@ -169,6 +170,7 @@
    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 @@ -237,7 +239,6 @@
    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 @@ -268,7 +269,6 @@
    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	Mon Oct 25 13:34:57 2010 +0200
     3.2 +++ b/src/HOL/Main.thy	Mon Oct 25 13:34:57 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
     3.8 +imports Plain Record Predicate_Compile Nitpick SMT Quotient
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Plain.thy	Mon Oct 25 13:34:57 2010 +0200
     4.2 +++ b/src/HOL/Plain.thy	Mon Oct 25 13:34:57 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 Metis
     4.8 +imports Datatype FunDef Extraction Sledgehammer
     4.9  begin
    4.10  
    4.11  text {*
     5.1 --- a/src/HOL/Refute.thy	Mon Oct 25 13:34:57 2010 +0200
     5.2 +++ b/src/HOL/Refute.thy	Mon Oct 25 13:34:57 2010 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  header {* Refute *}
     5.5  
     5.6  theory Refute
     5.7 -imports Hilbert_Choice List Sledgehammer
     5.8 +imports Hilbert_Choice List
     5.9  uses "Tools/refute.ML"
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Sledgehammer.thy	Mon Oct 25 13:34:57 2010 +0200
     6.2 +++ b/src/HOL/Sledgehammer.thy	Mon Oct 25 13:34:57 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
     6.8 +imports ATP Metis
     6.9  uses "Tools/Sledgehammer/sledgehammer_util.ML"
    6.10       "Tools/Sledgehammer/sledgehammer_filter.ML"
    6.11       "Tools/Sledgehammer/sledgehammer_atp_translate.ML"