22 val map_facts: ('a -> 'att) -> |
22 val map_facts: ('a -> 'att) -> |
23 (('c * 'a list) * ('d * 'a list) list) list -> |
23 (('c * 'a list) * ('d * 'a list) list) list -> |
24 (('c * 'att list) * ('d * 'att list) list) list |
24 (('c * 'att list) * ('d * 'att list) list) list |
25 val crude_closure: Proof.context -> src -> src |
25 val crude_closure: Proof.context -> src -> src |
26 val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory |
26 val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory |
27 val syntax: (Context.generic * Args.T list -> |
27 val syntax: attribute context_parser -> src -> attribute |
28 attribute * (Context.generic * Args.T list)) -> src -> attribute |
|
29 val no_args: attribute -> src -> attribute |
28 val no_args: attribute -> src -> attribute |
30 val add_del_args: attribute -> attribute -> src -> attribute |
29 val add_del_args: attribute -> attribute -> src -> attribute |
31 val thm_sel: Args.T list -> Facts.interval list * Args.T list |
30 val thm_sel: Facts.interval list parser |
32 val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list) |
31 val thm: thm context_parser |
33 val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) |
32 val thms: thm list context_parser |
34 val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) |
33 val multi_thm: thm list context_parser |
35 val print_configs: Proof.context -> unit |
34 val print_configs: Proof.context -> unit |
36 val internal: (morphism -> attribute) -> src |
35 val internal: (morphism -> attribute) -> src |
37 val register_config: Config.value Config.T -> theory -> theory |
36 val register_config: Config.value Config.T -> theory -> theory |
38 val config_bool: bstring -> bool -> bool Config.T * (theory -> theory) |
37 val config_bool: bstring -> bool -> bool Config.T * (theory -> theory) |
39 val config_int: bstring -> int -> int Config.T * (theory -> theory) |
38 val config_int: bstring -> int -> int Config.T * (theory -> theory) |