equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/TFL/thry.ML |
1 (* Title: HOL/Tools/TFL/thry.ML |
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
2 Author: Konrad Slind, Cambridge University Computer Laboratory |
4 Copyright 1997 University of Cambridge |
|
5 *) |
3 *) |
6 |
4 |
7 signature THRY = |
5 signature THRY = |
8 sig |
6 sig |
9 val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list |
7 val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list |