TFL/thry.sig
author nipkow
Fri Oct 09 14:19:13 1998 +0200 (1998-10-09)
changeset 5633 fb7fa1b154c4
parent 3405 2cccd0e3e9ea
permissions -rw-r--r--
Added a few breaks in error text.
     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