TFL/thry.sig
author paulson
Thu, 05 Jun 1997 13:27:28 +0200
changeset 3405 2cccd0e3e9ea
parent 3353 9112a2efb9a3
permissions -rw-r--r--
Numerous simplifications and removal of HOL-isms Addition of the "simpset" feature (replacing references to \!simpset)

(*  Title:      TFL/thry
    ID:         $Id$
    Author:     Konrad Slind, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge
*)

signature Thry_sig =
sig
  val match_term : theory -> term -> term 
                    -> (term*term)list * (typ*typ)list

  val match_type : theory -> typ -> typ -> (typ*typ)list

  val typecheck : theory -> term -> cterm

  (* Datatype facts of various flavours *)
  val match_info: theory -> string -> {constructors:term list,
                                     case_const:term} option

  val induct_info: theory -> string -> {constructors:term list,
                                      nchotomy:thm} option

  val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}

end;