equal
deleted
inserted
replaced
49 val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> |
49 val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> |
50 local_theory -> local_theory |
50 local_theory -> local_theory |
51 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
51 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
52 val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
52 val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
53 val theorems: string -> |
53 val theorems: string -> |
54 (Attrib.binding * (thm list * Token.src list) list) list -> |
54 (Attrib.binding * Attrib.thms) list -> |
55 (binding * typ option * mixfix) list -> |
55 (binding * typ option * mixfix) list -> |
56 bool -> local_theory -> (string * thm list) list * local_theory |
56 bool -> local_theory -> (string * thm list) list * local_theory |
57 val theorems_cmd: string -> |
57 val theorems_cmd: string -> |
58 (Attrib.binding * (Facts.ref * Token.src list) list) list -> |
58 (Attrib.binding * (Facts.ref * Token.src list) list) list -> |
59 (binding * string option * mixfix) list -> |
59 (binding * string option * mixfix) list -> |