changeset 3302 | 404fe31fd8d2 |
parent 3245 | 241838c01caf |
child 3333 | 0bbf06e86c06 |
3301:cdcc4d5602b6 | 3302:404fe31fd8d2 |
---|---|
1 (* Title: TFL/tfl |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 Main TFL functor |
|
7 *) |
|
8 |
|
1 signature TFL_sig = |
9 signature TFL_sig = |
2 sig |
10 sig |
3 structure Rules: Rules_sig |
11 structure Rules: Rules_sig |
4 structure Thms : Thms_sig |
12 structure Thms : Thms_sig |
5 structure Thry : Thry_sig |
13 structure Thry : Thry_sig |