changeset 38632 | 9cde57cdd0e3 |
parent 38610 | 5266689abbc1 |
child 38652 | e063be321438 |
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Sun Aug 22 09:43:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Sun Aug 22 14:27:30 2010 +0200 @@ -8,6 +8,7 @@ signature CLAUSIFIER = sig val transform_elim_theorem : thm -> thm + val extensionalize_theorem : thm -> thm val introduce_combinators_in_cterm : cterm -> thm val introduce_combinators_in_theorem : thm -> thm val cnf_axiom: theory -> thm -> thm list