src/Pure/Proof/proof_syntax.ML
changeset 11839 3ef83c265aca
parent 11640 be1bc3b88480
child 12909 d3ad295a087a
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Oct 19 22:01:25 2001 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Oct 19 22:02:02 2001 +0200
     1.3 @@ -70,6 +70,8 @@
     1.4        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
     1.5         ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
     1.6         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
     1.7 +  |> Sign.add_modesyntax_i (("latex", false),
     1.8 +      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))])
     1.9    |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    1.10        [(Syntax.mk_appl (Constant "_Lam")
    1.11            [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],