TFL/thry.sig
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3405 2cccd0e3e9ea
permissions -rw-r--r--
tidying
     1 (*  Title:      TFL/thry
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 signature Thry_sig =
     8 sig
     9   val match_term : theory -> term -> term 
    10                     -> (term*term)list * (typ*typ)list
    11 
    12   val match_type : theory -> typ -> typ -> (typ*typ)list
    13 
    14   val typecheck : theory -> term -> cterm
    15 
    16   (* Datatype facts of various flavours *)
    17   val match_info: theory -> string -> {constructors:term list,
    18                                      case_const:term} option
    19 
    20   val induct_info: theory -> string -> {constructors:term list,
    21                                       nchotomy:thm} option
    22 
    23   val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
    24 
    25 end;
    26 
    27