92 val no_base_names: theory -> theory |
92 val no_base_names: theory -> theory |
93 val custom_accesses: (string list -> string list list) -> theory -> theory |
93 val custom_accesses: (string list -> string list list) -> theory -> theory |
94 val set_policy: (string -> bstring -> string) * (string list -> string list list) -> |
94 val set_policy: (string -> bstring -> string) * (string list -> string list list) -> |
95 theory -> theory |
95 theory -> theory |
96 val restore_naming: theory -> theory -> theory |
96 val restore_naming: theory -> theory -> theory |
97 val hide_space: bool -> string * xstring list -> theory -> theory |
97 val hide_classes: bool -> xstring list -> theory -> theory |
98 val hide_space_i: bool -> string * string list -> theory -> theory |
98 val hide_classes_i: bool -> string list -> theory -> theory |
99 val hide_classes: bool -> string list -> theory -> theory |
99 val hide_types: bool -> xstring list -> theory -> theory |
100 val hide_types: bool -> string list -> theory -> theory |
100 val hide_types_i: bool -> string list -> theory -> theory |
101 val hide_consts: bool -> string list -> theory -> theory |
101 val hide_consts: bool -> xstring list -> theory -> theory |
|
102 val hide_consts_i: bool -> string list -> theory -> theory |
102 val add_name: string -> theory -> theory |
103 val add_name: string -> theory -> theory |
103 val copy: theory -> theory |
104 val copy: theory -> theory |
104 val prep_ext: theory -> theory |
105 val prep_ext: theory -> theory |
105 val prep_ext_merge: theory list -> theory |
106 val prep_ext_merge: theory list -> theory |
106 val requires: theory -> string -> string -> unit |
107 val requires: theory -> string -> string -> unit |
233 val qualified_names = ext_sign (K Sign.qualified_names) (); |
234 val qualified_names = ext_sign (K Sign.qualified_names) (); |
234 val no_base_names = ext_sign (K Sign.no_base_names) (); |
235 val no_base_names = ext_sign (K Sign.no_base_names) (); |
235 val custom_accesses = ext_sign Sign.custom_accesses; |
236 val custom_accesses = ext_sign Sign.custom_accesses; |
236 val set_policy = ext_sign Sign.set_policy; |
237 val set_policy = ext_sign Sign.set_policy; |
237 val restore_naming = ext_sign Sign.restore_naming o sign_of; |
238 val restore_naming = ext_sign Sign.restore_naming o sign_of; |
238 val hide_space = ext_sign o Sign.hide_space; |
239 val hide_classes = ext_sign o Sign.hide_classes; |
239 val hide_space_i = ext_sign o Sign.hide_space_i; |
240 val hide_classes_i = ext_sign o Sign.hide_classes_i; |
240 fun hide_classes b = curry (hide_space_i b) Sign.classK; |
241 val hide_types = ext_sign o Sign.hide_types; |
241 fun hide_types b = curry (hide_space_i b) Sign.typeK; |
242 val hide_types_i = ext_sign o Sign.hide_types_i; |
242 fun hide_consts b = curry (hide_space_i b) Sign.constK; |
243 val hide_consts = ext_sign o Sign.hide_consts; |
|
244 val hide_consts_i = ext_sign o Sign.hide_consts_i; |
243 val add_name = ext_sign Sign.add_name; |
245 val add_name = ext_sign Sign.add_name; |
244 val copy = ext_sign (K Sign.copy) (); |
246 val copy = ext_sign (K Sign.copy) (); |
245 val prep_ext = ext_sign (K Sign.prep_ext) (); |
247 val prep_ext = ext_sign (K Sign.prep_ext) (); |
246 |
248 |
247 |
249 |