src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
changeset 50263 0b430064296a
parent 50259 9c64a52ae499
child 51179 0d5f8812856f
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed Nov 28 12:25:43 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed Nov 28 12:25:43 2012 +0100
     1.3 @@ -1,3 +1,11 @@
     1.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Author:     Steffen Juilf Smolka, TU Muenchen
     1.7 +
     1.8 +Supplement term with explicit type constraints that show up as 
     1.9 +type annotations when printing the term.
    1.10 +*)
    1.11 +
    1.12  signature SLEDGEHAMMER_ANNOTATE =
    1.13  sig
    1.14    val annotate_types : Proof.context -> term -> term