equal
deleted
inserted
replaced
70 type proto_const_syntax |
70 type proto_const_syntax |
71 type const_syntax |
71 type const_syntax |
72 val parse_infix: ('a -> 'b) -> lrx * int -> string |
72 val parse_infix: ('a -> 'b) -> lrx * int -> string |
73 -> int * ((fixity -> 'b -> Pretty.T) |
73 -> int * ((fixity -> 'b -> Pretty.T) |
74 -> fixity -> 'a list -> Pretty.T) |
74 -> fixity -> 'a list -> Pretty.T) |
75 val parse_syntax: ('a -> 'b) -> OuterParse.token list |
75 val parse_syntax: ('a -> 'b) -> Token.T list |
76 -> (int * ((fixity -> 'b -> Pretty.T) |
76 -> (int * ((fixity -> 'b -> Pretty.T) |
77 -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list |
77 -> fixity -> 'a list -> Pretty.T)) option * Token.T list |
78 val simple_const_syntax: simple_const_syntax -> proto_const_syntax |
78 val simple_const_syntax: simple_const_syntax -> proto_const_syntax |
79 val activate_const_syntax: theory -> literals |
79 val activate_const_syntax: theory -> literals |
80 -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming |
80 -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming |
81 val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list) |
81 val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list) |
82 -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) |
82 -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) |