equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature NITPICK = |
8 signature NITPICK = |
9 sig |
9 sig |
10 type styp = Nitpick_Util.styp |
10 type styp = Nitpick_Util.styp |
|
11 type term_postprocessor = Nitpick_Model.term_postprocessor |
11 type params = { |
12 type params = { |
12 cards_assigns: (typ option * int list) list, |
13 cards_assigns: (typ option * int list) list, |
13 maxes_assigns: (styp option * int list) list, |
14 maxes_assigns: (styp option * int list) list, |
14 iters_assigns: (styp option * int list) list, |
15 iters_assigns: (styp option * int list) list, |
15 bitss: int list, |
16 bitss: int list, |
56 |
57 |
57 val register_frac_type : string -> (string * string) list -> theory -> theory |
58 val register_frac_type : string -> (string * string) list -> theory -> theory |
58 val unregister_frac_type : string -> theory -> theory |
59 val unregister_frac_type : string -> theory -> theory |
59 val register_codatatype : typ -> string -> styp list -> theory -> theory |
60 val register_codatatype : typ -> string -> styp list -> theory -> theory |
60 val unregister_codatatype : typ -> theory -> theory |
61 val unregister_codatatype : typ -> theory -> theory |
|
62 val register_term_postprocessor : |
|
63 typ -> term_postprocessor -> theory -> theory |
|
64 val unregister_term_postprocessor : typ -> theory -> theory |
61 val pick_nits_in_term : |
65 val pick_nits_in_term : |
62 Proof.state -> params -> bool -> int -> int -> int -> (term * term) list |
66 Proof.state -> params -> bool -> int -> int -> int -> (term * term) list |
63 -> term list -> term -> string * Proof.state |
67 -> term list -> term -> string * Proof.state |
64 val pick_nits_in_subgoal : |
68 val pick_nits_in_subgoal : |
65 Proof.state -> params -> bool -> int -> int -> string * Proof.state |
69 Proof.state -> params -> bool -> int -> int -> string * Proof.state |