68 [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)), |
68 [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)), |
69 (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)), |
69 (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)), |
70 (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))] |
70 (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))] |
71 |> Sign.add_modesyntax_i ("latex", false) |
71 |> Sign.add_modesyntax_i ("latex", false) |
72 [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))] |
72 [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))] |
73 |> Sign.add_trrules_i (map Syntax.ParsePrintRule |
73 |> Sign.add_trrules (map Syntax.Parse_Print_Rule |
74 [(Syntax.mk_appl (Constant "_Lam") |
74 [(Syntax.mk_appl (Constant "_Lam") |
75 [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"], |
75 [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"], |
76 Syntax.mk_appl (Constant "_Lam") |
76 Syntax.mk_appl (Constant "_Lam") |
77 [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]), |
77 [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]), |
78 (Syntax.mk_appl (Constant "_Lam") |
78 (Syntax.mk_appl (Constant "_Lam") |