author | paulson |
Thu, 22 May 1997 15:13:16 +0200 | |
changeset 3302 | 404fe31fd8d2 |
parent 3245 | 241838c01caf |
child 3353 | 9112a2efb9a3 |
permissions | -rw-r--r-- |
3302 | 1 |
(* Title: TFL/mask |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 |
Copyright 1997 University of Cambridge |
|
5 |
||
6 |
Compile the TFL system |
|
7 |
*) |
|
2112 | 8 |
|
9 |
(* Portability stuff *) |
|
10 |
nonfix prefix; |
|
11 |
use"mask.sig"; |
|
12 |
use"mask.sml"; |
|
13 |
||
14 |
(* Establish a base of common and/or helpful functions. *) |
|
15 |
use "utils.sig"; |
|
16 |
||
17 |
(* Get the specifications - these are independent of any system *) |
|
18 |
use "usyntax.sig"; |
|
19 |
use "rules.sig"; |
|
20 |
use "thry.sig"; |
|
21 |
use "thms.sig"; |
|
22 |
use "tfl.sig"; |
|
23 |
||
24 |
(*---------------------------------------------------------------------------- |
|
25 |
* Load the TFL functor - this is defined totally in terms of the |
|
26 |
* above interfaces. |
|
27 |
*---------------------------------------------------------------------------*) |
|
28 |
||
29 |
use "tfl.sml"; |
|
30 |
||
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
31 |
use "utils.sml"; |
2112 | 32 |
|
33 |
(*---------------------------------------------------------------------------- |
|
34 |
* Supply implementations |
|
35 |
*---------------------------------------------------------------------------*) |
|
36 |
||
37 |
use "usyntax.sml"; |
|
38 |
use "thms.sml"; |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
39 |
use"dcterm.sml"; |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
40 |
use"rules.new.sml"; |
2112 | 41 |
use "thry.sml"; |
42 |
||
43 |
||
44 |
(*---------------------------------------------------------------------------- |
|
45 |
* Link system and specialize for Isabelle |
|
46 |
*---------------------------------------------------------------------------*) |
|
47 |
structure Prim = TFL(structure Rules = FastRules |
|
48 |
structure Thms = Thms |
|
49 |
structure Thry = Thry); |
|
50 |
||
51 |
use"post.sml"; |