4 |
4 |
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
6 10 20 30 40 50 60 70 80 |
6 10 20 30 40 50 60 70 80 |
7 *) |
7 *) |
8 |
8 |
9 theory Atools imports Descript |
9 theory Atools imports Descript "../Interpret/Interpret" |
10 uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml") |
10 (* |
11 ("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml") |
11 uses ("../Interpret/mstools.sml")("../Interpret/ctree.sml") |
12 ("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml") |
12 ("../Interpret/ptyps.sml")("../Interpret/generate.sml") |
13 ("Interpret/inform.sml")("Interpret/mathengine.sml") |
13 ("../Interpret/calchead.sml")("../Interpret/appl.sml") |
14 ("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml") |
14 ("../Interpret/rewtools.sml")("../Interpret/script.sml") |
15 ("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml") |
15 ("../Interpret/solve.sml")("../Interpret/inform.sml") |
16 ("Frontend/messages.sml")("Frontend/states.sml")("Frontend/interface.sml") |
16 ("../Interpret/mathengine.sml")("../xmlsrc/mathml.sml") |
17 ("print_exn_G.sml") |
17 ("../xmlsrc/datatypes.sml")("../xmlsrc/pbl-met-hierarchy.sml") |
|
18 ("../xmlsrc/thy-hierarchy.sml")("../xmlsrc/interface-xml.sml") |
|
19 ("../Frontend/messages.sml")("../Frontend/states.sml") |
|
20 ("../Frontend/interface.sml")("../print_exn_G.sml") |
|
21 *) |
18 begin |
22 begin |
19 use "Interpret/mstools.sml" |
23 (* |
20 use "Interpret/ctree.sml" |
24 use "../Interpret/mstools.sml" |
21 use "Interpret/ptyps.sml" (*^^^ need files for: fun prep_pbt, fun store_pbt*) |
25 use "../Interpret/ctree.sml" |
22 use "Interpret/generate.sml" |
26 use "../Interpret/ptyps.sml" (*^^^ need for: fun prep_pbt, fun store_pbt*) |
23 use "Interpret/calchead.sml" |
27 use "../Interpret/generate.sml" |
24 use "Interpret/appl.sml" |
28 use "../Interpret/calchead.sml" |
25 use "Interpret/rewtools.sml" |
29 use "../Interpret/appl.sml" |
26 use "Interpret/script.sml" |
30 use "../Interpret/rewtools.sml" |
27 use "Interpret/solve.sml" |
31 use "../Interpret/script.sml" |
28 use "Interpret/inform.sml" (*^^^ need files for: fun castab*) |
32 use "../Interpret/solve.sml" |
29 use "Interpret/mathengine.sml" |
33 use "../Interpret/inform.sml" (*^^^ need files for: fun castab*) |
30 |
34 use "../Interpret/mathengine.sml" |
31 use "xmlsrc/mathml.sml" |
35 |
32 use "xmlsrc/datatypes.sml" |
36 use "../xmlsrc/mathml.sml" |
33 use "xmlsrc/pbl-met-hierarchy.sml" |
37 use "../xmlsrc/datatypes.sml" |
34 use "xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*) |
38 use "../xmlsrc/pbl-met-hierarchy.sml" |
35 use "xmlsrc/interface-xml.sml" |
39 use "../xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*) |
36 |
40 use "../xmlsrc/interface-xml.sml" |
37 use "Frontend/messages.sml" |
41 |
38 use "Frontend/states.sml" (*^^^ need files for: val states in Test_Isac.thy*) |
42 use "../Frontend/messages.sml" |
39 use "Frontend/interface.sml" |
43 use "../Frontend/states.sml" (*^^^ need for: val states in Test_Isac.thy*) |
40 |
44 use "../Frontend/interface.sml" |
41 use "print_exn_G.sml" |
45 |
42 |
46 use "../print_exn_G.sml" |
|
47 *) |
43 consts |
48 consts |
44 |
49 |
45 Arbfix :: "real" |
50 Arbfix :: "real" |
46 Undef :: "real" |
51 Undef :: "real" |
47 dummy :: "real" |
52 dummy :: "real" |