equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature MESON_CLAUSIFY = |
8 signature MESON_CLAUSIFY = |
9 sig |
9 sig |
10 val new_skolem_var_prefix : string |
10 val new_skolem_var_prefix : string |
|
11 val new_nonskolem_var_prefix : string |
11 val extensionalize_theorem : thm -> thm |
12 val extensionalize_theorem : thm -> thm |
12 val introduce_combinators_in_cterm : cterm -> thm |
13 val introduce_combinators_in_cterm : cterm -> thm |
13 val introduce_combinators_in_theorem : thm -> thm |
14 val introduce_combinators_in_theorem : thm -> thm |
14 val to_definitional_cnf_with_quantifiers : theory -> thm -> thm |
15 val to_definitional_cnf_with_quantifiers : theory -> thm -> thm |
15 val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool |
16 val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool |