Lines Matching defs:prover
25 3: More detailed prover information: slice by slice
54 (* Making the Metis prover HOL specific. *)
255 (* Tactic interface to the metis prover. *)
334 (* Simple user interface to the metis prover. *)
337 fun prover ttac ths goal = Tactical.default_prover (goal, ttac ths);
339 val FO_METIS_PROVE = prover FO_METIS_TAC;
340 val FOT_METIS_PROVE = prover FOT_METIS_TAC;
341 val HO_METIS_PROVE = prover HO_METIS_TAC;
342 val HOT_METIS_PROVE = prover HOT_METIS_TAC;
343 val FULL_METIS_PROVE = prover FULL_METIS_TAC;
442 val METIS_PROVE = prover METIS_TAC;