Structure metisLib


Source File Identifier index Theory binding index

(* ========================================================================= *)
(* THE METIS LIBRARY                                                         *)
(* Created by Joe Hurd, July 2002                                            *)
(* ========================================================================= *)

signature metisLib =
sig

(* Top-level entry-point to the metis prover *)
val METIS_TAC   : Thm.thm list -> Tactic.tactic
val METIS_PROVE : Thm.thm list -> Term.term -> Thm.thm

end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1