equal
deleted
inserted
replaced
59 val qualified_names: theory -> theory |
59 val qualified_names: theory -> theory |
60 val sticky_prefix: string -> theory -> theory |
60 val sticky_prefix: string -> theory -> theory |
61 val set_policy: (string -> bstring -> string) * (string list -> string list list) -> |
61 val set_policy: (string -> bstring -> string) * (string list -> string list list) -> |
62 theory -> theory |
62 theory -> theory |
63 val restore_naming: theory -> theory -> theory |
63 val restore_naming: theory -> theory -> theory |
64 val hide_classes: bool -> xstring list -> theory -> theory |
|
65 val hide_classes_i: bool -> string list -> theory -> theory |
|
66 val hide_types: bool -> xstring list -> theory -> theory |
|
67 val hide_types_i: bool -> string list -> theory -> theory |
|
68 val hide_consts: bool -> xstring list -> theory -> theory |
|
69 val hide_consts_i: bool -> string list -> theory -> theory |
|
70 val hide_names: bool -> string * xstring list -> theory -> theory |
|
71 val hide_names_i: bool -> string * string list -> theory -> theory |
|
72 end |
64 end |
73 |
65 |
74 signature SIGN = |
66 signature SIGN = |
75 sig |
67 sig |
76 val init_data: theory -> theory |
68 val init_data: theory -> theory |
184 val read_prop: theory -> string -> term |
176 val read_prop: theory -> string -> term |
185 val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory |
177 val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory |
186 val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory |
178 val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory |
187 val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory |
179 val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory |
188 include SIGN_THEORY |
180 include SIGN_THEORY |
|
181 val hide_classes: bool -> xstring list -> theory -> theory |
|
182 val hide_classes_i: bool -> string list -> theory -> theory |
|
183 val hide_types: bool -> xstring list -> theory -> theory |
|
184 val hide_types_i: bool -> string list -> theory -> theory |
|
185 val hide_consts: bool -> xstring list -> theory -> theory |
|
186 val hide_consts_i: bool -> string list -> theory -> theory |
|
187 val hide_names: bool -> string * xstring list -> theory -> theory |
|
188 val hide_names_i: bool -> string * string list -> theory -> theory |
189 end |
189 end |
190 |
190 |
191 structure Sign: SIGN = |
191 structure Sign: SIGN = |
192 struct |
192 struct |
193 |
193 |