factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
authorblanchet
Tue Oct 05 11:10:37 2010 +0200 (2010-10-05)
changeset 39951ff60a6e4edfe
parent 39950 f3c4849868b8
child 39952 7fb79905ed72
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
src/HOL/ATP.thy
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ATP.thy	Tue Oct 05 11:10:37 2010 +0200
     1.3 @@ -0,0 +1,17 @@
     1.4 +(*  Title:      HOL/ATP.thy
     1.5 +    Author:     Fabian Immler, TU Muenchen
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Sledgehammer: Isabelle--ATP Linkup *}
    1.10 +
    1.11 +theory ATP
    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
    1.19 +
    1.20 +end
     2.1 --- a/src/HOL/IsaMakefile	Tue Oct 05 10:59:12 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Oct 05 11:10:37 2010 +0200
     2.3 @@ -234,6 +234,7 @@
     2.4  	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
     2.5  
     2.6  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
     2.7 +  ATP.thy \
     2.8    Big_Operators.thy \
     2.9    Code_Evaluation.thy \
    2.10    Code_Numeral.thy \
     3.1 --- a/src/HOL/Sledgehammer.thy	Tue Oct 05 10:59:12 2010 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Tue Oct 05 11:10:37 2010 +0200
     3.3 @@ -1,18 +1,14 @@
     3.4  (*  Title:      HOL/Sledgehammer.thy
     3.5      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3.6      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3.7 -    Author:     Fabian Immler, TU Muenchen
     3.8      Author:     Jasmin Blanchette, TU Muenchen
     3.9  *)
    3.10  
    3.11  header {* Sledgehammer: Isabelle--ATP Linkup *}
    3.12  
    3.13  theory Sledgehammer
    3.14 -imports Plain
    3.15 -uses "Tools/ATP/atp_problem.ML"
    3.16 -     "Tools/ATP/atp_proof.ML"
    3.17 -     "Tools/ATP/atp_systems.ML"
    3.18 -     "Tools/Sledgehammer/sledgehammer_util.ML"
    3.19 +imports ATP
    3.20 +uses "Tools/Sledgehammer/sledgehammer_util.ML"
    3.21       "Tools/Sledgehammer/sledgehammer_filter.ML"
    3.22       "Tools/Sledgehammer/sledgehammer_translate.ML"
    3.23       "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    3.24 @@ -22,8 +18,7 @@
    3.25  begin
    3.26  
    3.27  setup {*
    3.28 -  ATP_Systems.setup
    3.29 -  #> Sledgehammer.setup
    3.30 +  Sledgehammer.setup
    3.31    #> Sledgehammer_Isar.setup
    3.32  *}
    3.33