src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
changeset 55212 5832470d956e
parent 55205 8450622db0c5
child 55213 dcb36a2540bc
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:07:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:10:39 2014 +0100
     1.3 @@ -1,17 +1,15 @@
     1.4  (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
     1.5 +    Author:     Steffen Juilf Smolka, TU Muenchen
     1.6      Author:     Jasmin Blanchette, TU Muenchen
     1.7 -    Author:     Steffen Juilf Smolka, TU Muenchen
     1.8  
     1.9 -Supplements term with a locally minmal, complete set of type constraints.
    1.10 -Complete: The constraints suffice to infer the term's types.
    1.11 -Minimal: Reducing the set of constraints further will make it incomplete.
    1.12 +Supplements term with a locally minmal, complete set of type constraints. Complete: The constraints
    1.13 +suffice to infer the term's types. Minimal: Reducing the set of constraints further will make it
    1.14 +incomplete.
    1.15  
    1.16 -When configuring the pretty printer appropriately, the constraints will show up
    1.17 -as type annotations when printing the term. This allows the term to be printed
    1.18 -and reparsed without a change of types.
    1.19 +When configuring the pretty printer appropriately, the constraints will show up as type annotations
    1.20 +when printing the term. This allows the term to be printed and reparsed without a change of types.
    1.21  
    1.22 -NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
    1.23 -syntax.
    1.24 +NOTE: Terms should be unchecked before calling annotate_types to avoid awkward syntax.
    1.25  *)
    1.26  
    1.27  signature SLEDGEHAMMER_ISAR_ANNOTATE =