changeset 38050 | 0511f2e62363 |
parent 38045 | f367847f5068 |
child 38083 | c4b57f68ddb3 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 19:23:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 19:42:11 2010 +0200 @@ -9,6 +9,9 @@ sig type params = Sledgehammer.params + val minimize_theorems : + params -> int -> int -> Proof.state -> (string * thm list) list + -> (string * thm list) list option * string val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit end;