# HG changeset patch
# User blanchet
# Date 1284647063 -7200
# Node ID bb4fb9ffe2d173d90507123a3bda09870accf992
# Parent  bf7dd4902321f8682c83a78cbe8bd7be82b57675
added new "Metis_Reconstruct" module, temporarily empty

diff -r bf7dd4902321 -r bb4fb9ffe2d1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 16 16:12:02 2010 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 16 16:24:23 2010 +0200
@@ -316,6 +316,7 @@
   Tools/semiring_normalizer.ML \
   Tools/Sledgehammer/clausifier.ML \
   Tools/Sledgehammer/meson_tactic.ML \
+  Tools/Sledgehammer/metis_reconstruct.ML \
   Tools/Sledgehammer/metis_translate.ML \
   Tools/Sledgehammer/metis_tactics.ML \
   Tools/Sledgehammer/sledgehammer.ML \
diff -r bf7dd4902321 -r bb4fb9ffe2d1 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Sep 16 16:12:02 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Sep 16 16:24:23 2010 +0200
@@ -17,6 +17,7 @@
   ("Tools/Sledgehammer/clausifier.ML")
   ("Tools/Sledgehammer/meson_tactic.ML")
   ("Tools/Sledgehammer/metis_translate.ML")
+  ("Tools/Sledgehammer/metis_reconstruct.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
   ("Tools/Sledgehammer/sledgehammer_util.ML")
   ("Tools/Sledgehammer/sledgehammer_filter.ML")
@@ -103,6 +104,7 @@
 setup Meson_Tactic.setup
 
 use "Tools/Sledgehammer/metis_translate.ML"
+use "Tools/Sledgehammer/metis_reconstruct.ML"
 use "Tools/Sledgehammer/metis_tactics.ML"
 setup Metis_Tactics.setup
 
diff -r bf7dd4902321 -r bb4fb9ffe2d1 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 16 16:24:23 2010 +0200
@@ -0,0 +1,17 @@
+(*  Title:      HOL/Tools/Sledgehammer/metis_reconstruct.ML
+    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   Cambridge University 2007
+
+Proof reconstruction for Metis.
+*)
+
+signature METIS_RECONSTRUCT =
+sig
+end;
+
+structure Metis_Reconstruct : METIS_RECONSTRUCT =
+struct
+
+end;
diff -r bf7dd4902321 -r bb4fb9ffe2d1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 16:12:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 16:24:23 2010 +0200
@@ -3,7 +3,7 @@
     Author:     Claire Quigley, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
-Transfer of proofs from external provers.
+Proof reconstruction for Sledgehammer.
 *)
 
 signature SLEDGEHAMMER_RECONSTRUCT =