added new "Metis_Reconstruct" module, temporarily empty
authorblanchet
Thu Sep 16 16:24:23 2010 +0200 (2010-09-16)
changeset 39495bb4fb9ffe2d1
parent 39494 bf7dd4902321
child 39496 a52a4e4399c1
added new "Metis_Reconstruct" module, temporarily empty
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 16 16:12:02 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Sep 16 16:24:23 2010 +0200
     1.3 @@ -316,6 +316,7 @@
     1.4    Tools/semiring_normalizer.ML \
     1.5    Tools/Sledgehammer/clausifier.ML \
     1.6    Tools/Sledgehammer/meson_tactic.ML \
     1.7 +  Tools/Sledgehammer/metis_reconstruct.ML \
     1.8    Tools/Sledgehammer/metis_translate.ML \
     1.9    Tools/Sledgehammer/metis_tactics.ML \
    1.10    Tools/Sledgehammer/sledgehammer.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 16 16:12:02 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 16 16:24:23 2010 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    ("Tools/Sledgehammer/clausifier.ML")
     2.5    ("Tools/Sledgehammer/meson_tactic.ML")
     2.6    ("Tools/Sledgehammer/metis_translate.ML")
     2.7 +  ("Tools/Sledgehammer/metis_reconstruct.ML")
     2.8    ("Tools/Sledgehammer/metis_tactics.ML")
     2.9    ("Tools/Sledgehammer/sledgehammer_util.ML")
    2.10    ("Tools/Sledgehammer/sledgehammer_filter.ML")
    2.11 @@ -103,6 +104,7 @@
    2.12  setup Meson_Tactic.setup
    2.13  
    2.14  use "Tools/Sledgehammer/metis_translate.ML"
    2.15 +use "Tools/Sledgehammer/metis_reconstruct.ML"
    2.16  use "Tools/Sledgehammer/metis_tactics.ML"
    2.17  setup Metis_Tactics.setup
    2.18  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 16 16:24:23 2010 +0200
     3.3 @@ -0,0 +1,17 @@
     3.4 +(*  Title:      HOL/Tools/Sledgehammer/metis_reconstruct.ML
     3.5 +    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     3.6 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3.7 +    Author:     Jasmin Blanchette, TU Muenchen
     3.8 +    Copyright   Cambridge University 2007
     3.9 +
    3.10 +Proof reconstruction for Metis.
    3.11 +*)
    3.12 +
    3.13 +signature METIS_RECONSTRUCT =
    3.14 +sig
    3.15 +end;
    3.16 +
    3.17 +structure Metis_Reconstruct : METIS_RECONSTRUCT =
    3.18 +struct
    3.19 +
    3.20 +end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 16:12:02 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 16:24:23 2010 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Claire Quigley, Cambridge University Computer Laboratory
     4.5      Author:     Jasmin Blanchette, TU Muenchen
     4.6  
     4.7 -Transfer of proofs from external provers.
     4.8 +Proof reconstruction for Sledgehammer.
     4.9  *)
    4.10  
    4.11  signature SLEDGEHAMMER_RECONSTRUCT =