Tuned indentation of abstractions.
authorberghofe
Sun Sep 30 13:42:00 2001 +0200 (2001-09-30)
changeset 11640be1bc3b88480
parent 11639 4213422388c4
child 11641 0c248bed5225
Tuned indentation of abstractions.
src/Pure/Proof/proof_syntax.ML
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 28 21:45:40 2001 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Sep 30 13:42:00 2001 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4         ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn)]
     1.5    |> Sign.add_nonterminals ["param", "params"]
     1.6    |> Sign.add_syntax_i
     1.7 -      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(3Lam _./ _)", [0, 3], 3)),
     1.8 +      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
     1.9         ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    1.10         ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    1.11         ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
    1.12 @@ -67,7 +67,7 @@
    1.13         ("", idtT --> paramsT, Delimfix "_"),
    1.14         ("", paramT --> paramsT, Delimfix "_")]
    1.15    |> Sign.add_modesyntax_i (("xsymbols", true),
    1.16 -      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(3\\<Lambda>_./ _)", [0, 3], 3)),
    1.17 +      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
    1.18         ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    1.19         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
    1.20    |> Sign.add_trrules_i (map Syntax.ParsePrintRule