author | paulson |
Tue, 27 May 1997 13:22:30 +0200 | |
changeset 3353 | 9112a2efb9a3 |
parent 3302 | 404fe31fd8d2 |
child 3405 | 2cccd0e3e9ea |
permissions | -rw-r--r-- |
3302 | 1 |
(* Title: TFL/thry |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 |
Copyright 1997 University of Cambridge |
|
5 |
*) |
|
6 |
||
2112 | 7 |
signature Thry_sig = |
8 |
sig |
|
9 |
structure USyntax : USyntax_sig |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
10 |
val match_term : theory -> term -> term |
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3302
diff
changeset
|
11 |
-> (term*term)list * (typ*typ)list |
2112 | 12 |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3302
diff
changeset
|
13 |
val match_type : theory -> typ -> typ -> (typ*typ)list |
2112 | 14 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
15 |
val typecheck : theory -> term -> cterm |
2112 | 16 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
17 |
val make_definition: theory -> string -> term -> thm * theory |
2112 | 18 |
|
19 |
(* Datatype facts of various flavours *) |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
20 |
val match_info: theory -> string -> {constructors:term list, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
21 |
case_const:term} option |
2112 | 22 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
23 |
val induct_info: theory -> string -> {constructors:term list, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
24 |
nchotomy:thm} option |
2112 | 25 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
26 |
val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list} |
2112 | 27 |
|
28 |
end; |
|
29 |
||
30 |