equal
deleted
inserted
replaced
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 |
|