TFL/thry.sig
author paulson
Tue, 20 May 1997 11:49:57 +0200
changeset 3245 241838c01caf
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
permissions -rw-r--r--
Removal of redundant code (unused or already present in Isabelle. This eliminates HOL compatibility but makes the code smaller and more readable

signature Thry_sig =
sig
  type 'a binding

  structure USyntax : USyntax_sig
  val match_term : theory -> term -> term 
                    -> term binding list * typ binding list

  val match_type : theory -> typ -> typ -> typ binding list

  val typecheck : theory -> term -> cterm

  val make_definition: theory -> string -> term -> thm * theory

  (* 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;