equal
deleted
inserted
replaced
5 use"mask.sig"; |
5 use"mask.sig"; |
6 use"mask.sml"; |
6 use"mask.sml"; |
7 |
7 |
8 (* Establish a base of common and/or helpful functions. *) |
8 (* Establish a base of common and/or helpful functions. *) |
9 use "utils.sig"; |
9 use "utils.sig"; |
10 use "utils.sml"; |
|
11 |
10 |
12 (* Get the specifications - these are independent of any system *) |
11 (* Get the specifications - these are independent of any system *) |
13 use "usyntax.sig"; |
12 use "usyntax.sig"; |
14 use "rules.sig"; |
13 use "rules.sig"; |
15 use "thry.sig"; |
14 use "thry.sig"; |
21 * above interfaces. |
20 * above interfaces. |
22 *---------------------------------------------------------------------------*) |
21 *---------------------------------------------------------------------------*) |
23 |
22 |
24 use "tfl.sml"; |
23 use "tfl.sml"; |
25 |
24 |
26 structure Utils = UTILS(val int_to_string = string_of_int); |
25 use "utils.sml"; |
27 |
26 |
28 (*---------------------------------------------------------------------------- |
27 (*---------------------------------------------------------------------------- |
29 * Supply implementations |
28 * Supply implementations |
30 *---------------------------------------------------------------------------*) |
29 *---------------------------------------------------------------------------*) |
31 |
30 |
32 (* Ignore "Time" exception raised at end of building theory. *) |
|
33 use "usyntax.sml"; |
31 use "usyntax.sml"; |
34 use "thms.sml"; |
32 use "thms.sml"; |
35 use"dcterm.sml"; use"rules.new.sml"; |
33 use"dcterm.sml"; |
|
34 use"rules.new.sml"; |
36 use "thry.sml"; |
35 use "thry.sml"; |
37 |
36 |
38 |
37 |
39 (*---------------------------------------------------------------------------- |
38 (*---------------------------------------------------------------------------- |
40 * Link system and specialize for Isabelle |
39 * Link system and specialize for Isabelle |