TFL/thry.sig
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 3405 2cccd0e3e9ea
permissions -rw-r--r--
adapted extend_trfunsT;
     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