# 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