--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 16:10:39 2014 +0100
@@ -1,17 +1,15 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
+ Author: Steffen Juilf Smolka, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-Supplements term with a locally minmal, complete set of type constraints.
-Complete: The constraints suffice to infer the term's types.
-Minimal: Reducing the set of constraints further will make it incomplete.
+Supplements term with a locally minmal, complete set of type constraints. Complete: The constraints
+suffice to infer the term's types. Minimal: Reducing the set of constraints further will make it
+incomplete.
-When configuring the pretty printer appropriately, the constraints will show up
-as type annotations when printing the term. This allows the term to be printed
-and reparsed without a change of types.
+When configuring the pretty printer appropriately, the constraints will show up as type annotations
+when printing the term. This allows the term to be printed and reparsed without a change of types.
-NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
-syntax.
+NOTE: Terms should be unchecked before calling annotate_types to avoid awkward syntax.
*)
signature SLEDGEHAMMER_ISAR_ANNOTATE =