# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 0b430064296ac62a2cd8109c75d5270f8179aa58
# Parent  6dc80eead659d470c33f5268e8126a10400dfcc6
added comments to new source files

diff -r 6dc80eead659 -r 0b430064296a src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
--- 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
diff -r 6dc80eead659 -r 0b430064296a src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML
--- 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
diff -r 6dc80eead659 -r 0b430064296a src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- 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