changeset 40181 | 3788b7adab36 |
parent 40144 | 23adc2138704 |
child 40341 | 03156257040f |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 26 12:23:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 26 13:16:43 2010 +0200 @@ -130,9 +130,6 @@ val extend = I fun merge p : T = AList.merge (op =) (K true) p) -(* FIXME: dummy *) -fun is_smt_solver_installed ctxt = true - fun remotify_prover_if_available_and_not_already_remote thy name = if String.isPrefix remote_prefix name then SOME name