--- a/src/HOL/Sledgehammer.thy Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Sledgehammer.thy
- Author: Lawrence C Paulson
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Jia Meng, NICTA
Author: Fabian Immler, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
--- a/src/HOL/Tools/ATP_Manager/atp_problem.ML Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/ATP_Manager/atp_problem.ML
- Author: Jia Meng, NICTA
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
TPTP syntax.
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/clausifier.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
Transformation of axiom rules (elim/intro/etc) into CNF forms.
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
MESON general tactic and proof method.
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/metis_clauses.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
Storing/printing FOL clauses and arity clauses. Typed equality is
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,7 @@
(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML
- Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
+ 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
HOL setup for the Metis prover.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
- Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 18:50:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 19:17:15 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
- Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Claire Quigley, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
Transfer of proofs from external provers.