TFL/thry.sig
changeset 3353 9112a2efb9a3
parent 3302 404fe31fd8d2
child 3405 2cccd0e3e9ea
equal deleted inserted replaced
3352:04502e5431fb 3353:9112a2efb9a3
     4     Copyright   1997  University of Cambridge
     4     Copyright   1997  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 signature Thry_sig =
     7 signature Thry_sig =
     8 sig
     8 sig
     9   type 'a binding
       
    10 
       
    11   structure USyntax : USyntax_sig
     9   structure USyntax : USyntax_sig
    12   val match_term : theory -> term -> term 
    10   val match_term : theory -> term -> term 
    13                     -> term binding list * typ binding list
    11                     -> (term*term)list * (typ*typ)list
    14 
    12 
    15   val match_type : theory -> typ -> typ -> typ binding list
    13   val match_type : theory -> typ -> typ -> (typ*typ)list
    16 
    14 
    17   val typecheck : theory -> term -> cterm
    15   val typecheck : theory -> term -> cterm
    18 
    16 
    19   val make_definition: theory -> string -> term -> thm * theory
    17   val make_definition: theory -> string -> term -> thm * theory
    20 
    18