--- a/src/HOL/ATP.thy Tue Oct 05 12:06:08 2010 +0200
+++ b/src/HOL/ATP.thy Tue Oct 05 12:50:45 2010 +0200
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
*)
-header {* Sledgehammer: Isabelle--ATP Linkup *}
+header {* Automatic Theorem Provers (ATPs) *}
theory ATP
imports Plain
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Oct 05 12:06:08 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Oct 05 12:50:45 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML
+(* Title: HOL/Tools/Metis/metis_reconstruct.ML
Author: Kong W. Susanto, Cambridge University Computer Laboratory
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 05 12:06:08 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 05 12:50:45 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML
+(* Title: HOL/Tools/Metis/metis_tactics.ML
Author: Kong W. Susanto, Cambridge University Computer Laboratory
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Oct 05 12:06:08 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Oct 05 12:50:45 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Sledgehammer/metis_translate.ML
+(* Title: HOL/Tools/Metis/metis_translate.ML
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Kong W. Susanto, Cambridge University Computer Laboratory
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Oct 05 12:06:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Oct 05 12:50:45 2010 +0200
@@ -1,6 +1,8 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
+
+Sledgehammer's relevance filter.
*)
signature SLEDGEHAMMER_FILTER =