changeset 42336 | d63d43e85879 |
parent 42335 | cb8aa792d138 |
child 42347 | 53e444ecb525 |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200 @@ -15,6 +15,7 @@ val introduce_combinators_in_theorem : thm -> thm val to_definitional_cnf_with_quantifiers : Proof.context -> thm -> thm val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool + val ss_only : thm list -> simpset val cnf_axiom : Proof.context -> bool -> int -> thm -> (thm * term) option * thm list end;