equal
deleted
inserted
replaced
14 val add_lessD: thm -> Context.generic -> Context.generic |
14 val add_lessD: thm -> Context.generic -> Context.generic |
15 val add_simps: thm list -> Context.generic -> Context.generic |
15 val add_simps: thm list -> Context.generic -> Context.generic |
16 val add_simprocs: simproc list -> Context.generic -> Context.generic |
16 val add_simprocs: simproc list -> Context.generic -> Context.generic |
17 val add_inj_const: string * typ -> Context.generic -> Context.generic |
17 val add_inj_const: string * typ -> Context.generic -> Context.generic |
18 val add_discrete_type: string -> Context.generic -> Context.generic |
18 val add_discrete_type: string -> Context.generic -> Context.generic |
19 val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> |
19 val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic |
20 Context.generic |
|
21 val setup: Context.generic -> Context.generic |
20 val setup: Context.generic -> Context.generic |
22 val global_setup: theory -> theory |
21 val global_setup: theory -> theory |
23 val split_limit: int Config.T |
22 val split_limit: int Config.T |
24 val neq_limit: int Config.T |
23 val neq_limit: int Config.T |
25 val trace: bool Unsynchronized.ref |
24 val trace: bool Unsynchronized.ref |