adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
authorbulwahn
Mon Nov 22 10:41:54 2010 +0100 (2010-11-22)
changeset 40634dc124a486f94
parent 40633 6cd611ceb64e
child 40635 47004929bc71
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
src/HOL/IsaMakefile
src/HOL/Mirabelle/Mirabelle_Test.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Nov 22 10:41:53 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Nov 22 10:41:54 2010 +0100
     1.3 @@ -1295,7 +1295,8 @@
     1.4    Mirabelle/Tools/mirabelle_metis.ML					\
     1.5    Mirabelle/Tools/mirabelle_quickcheck.ML				\
     1.6    Mirabelle/Tools/mirabelle_refute.ML					\
     1.7 -  Mirabelle/Tools/mirabelle_sledgehammer.ML
     1.8 +  Mirabelle/Tools/mirabelle_sledgehammer.ML 				\
     1.9 +  Mirabelle/Tools/sledgehammer_tactic.ML
    1.10  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    1.11  
    1.12  
     2.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Nov 22 10:41:53 2010 +0100
     2.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Nov 22 10:41:54 2010 +0100
     2.3 @@ -13,6 +13,7 @@
     2.4    "Tools/mirabelle_refute.ML"
     2.5    "Tools/mirabelle_sledgehammer.ML"
     2.6    "Tools/mirabelle_sledgehammer_filter.ML"
     2.7 +  "Tools/sledgehammer_tactic.ML"
     2.8  begin
     2.9  
    2.10  text {*