--- 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
@@ -1,9 +1,17 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_recontruct.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Basic data structures for representing and basic methods
+for dealing with Isar proof texts.
+*)
+
signature SLEDGEHAMMER_ISAR =
sig
val annotate_types : Proof.context -> term -> term
end
-structure Sledgehammer_Isar_Reconstruct (* : SLEDGEHAMMER_Isar *) =
+structure Sledgehammer_Isar_Reconstruct (* : SLEDGEHAMMER_Isar *) =
struct
type label = string * int
@@ -43,5 +51,4 @@
inc (fold (inc o metis_steps_recursive) cases 1)
| _ => I) proof 0
-
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
@@ -1,3 +1,10 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Shrinking of isar proofs reconstructed from ATP proofs.
+*)
+
signature SLEDGEHAMMER_SHRINK =
sig
type isar_step = Sledgehammer_Isar_Reconstruct.isar_step