TFL/thry.sig
author wenzelm
Wed, 25 Aug 1999 20:49:02 +0200
changeset 7357 d0e16da40ea2
parent 3405 2cccd0e3e9ea
permissions -rw-r--r--
proper bootstrap of HOL theory and packages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3302
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     1
(*  Title:      TFL/thry
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     2
    ID:         $Id$
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     4
    Copyright   1997  University of Cambridge
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     5
*)
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     6
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     7
signature Thry_sig =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     8
sig
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
     9
  val match_term : theory -> term -> term 
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3302
diff changeset
    10
                    -> (term*term)list * (typ*typ)list
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3302
diff changeset
    12
  val match_type : theory -> typ -> typ -> (typ*typ)list
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    14
  val typecheck : theory -> term -> cterm
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
  (* Datatype facts of various flavours *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    17
  val match_info: theory -> string -> {constructors:term list,
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    18
                                     case_const:term} option
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    20
  val induct_info: theory -> string -> {constructors:term list,
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    21
                                      nchotomy:thm} option
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    22
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    23
  val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27