tuned comments
authorblanchet
Tue Oct 05 12:50:45 2010 +0200 (2010-10-05)
changeset 3995888c9aa5666de
parent 39957 2f2d90cc31a2
child 39959 12eb8fe15b00
tuned comments
src/HOL/ATP.thy
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactics.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     1.1 --- a/src/HOL/ATP.thy	Tue Oct 05 12:06:08 2010 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue Oct 05 12:50:45 2010 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5  *)
     1.6  
     1.7 -header {* Sledgehammer: Isabelle--ATP Linkup *}
     1.8 +header {* Automatic Theorem Provers (ATPs) *}
     1.9  
    1.10  theory ATP
    1.11  imports Plain
     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 05 12:06:08 2010 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 05 12:50:45 2010 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Tools/Sledgehammer/metis_reconstruct.ML
     2.5 +(*  Title:      HOL/Tools/Metis/metis_reconstruct.ML
     2.6      Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     2.7      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     2.8      Author:     Jasmin Blanchette, TU Muenchen
     3.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 12:06:08 2010 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 12:50:45 2010 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
     3.5 +(*  Title:      HOL/Tools/Metis/metis_tactics.ML
     3.6      Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     3.7      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3.8      Author:     Jasmin Blanchette, TU Muenchen
     4.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 05 12:06:08 2010 +0200
     4.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 05 12:50:45 2010 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Tools/Sledgehammer/metis_translate.ML
     4.5 +(*  Title:      HOL/Tools/Metis/metis_translate.ML
     4.6      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4.7      Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     4.8      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Oct 05 12:06:08 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Oct 05 12:50:45 2010 +0200
     5.3 @@ -1,6 +1,8 @@
     5.4  (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     5.5      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     5.6      Author:     Jasmin Blanchette, TU Muenchen
     5.7 +
     5.8 +Sledgehammer's relevance filter.
     5.9  *)
    5.10  
    5.11  signature SLEDGEHAMMER_FILTER =