--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Wed Nov 28 12:25:43 2012 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Supplement term with explicit type constraints that show up as
+type annotations when printing the term.
+*)
+
signature SLEDGEHAMMER_ANNOTATE =
sig
val annotate_types : Proof.context -> term -> term