equal
deleted
inserted
replaced
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 structure USyntax : USyntax_sig |
|
10 val match_term : theory -> term -> term |
9 val match_term : theory -> term -> term |
11 -> (term*term)list * (typ*typ)list |
10 -> (term*term)list * (typ*typ)list |
12 |
11 |
13 val match_type : theory -> typ -> typ -> (typ*typ)list |
12 val match_type : theory -> typ -> typ -> (typ*typ)list |
14 |
13 |
15 val typecheck : theory -> term -> cterm |
14 val typecheck : theory -> term -> cterm |
16 |
|
17 val make_definition: theory -> string -> term -> thm * theory |
|
18 |
15 |
19 (* Datatype facts of various flavours *) |
16 (* Datatype facts of various flavours *) |
20 val match_info: theory -> string -> {constructors:term list, |
17 val match_info: theory -> string -> {constructors:term list, |
21 case_const:term} option |
18 case_const:term} option |
22 |
19 |