32 ML_file "~~/src/Tools/isac/ProgLang/program.sml" ? really separate? |
32 ML_file "~~/src/Tools/isac/ProgLang/program.sml" ? really separate? |
33 theory Atools imports Program |
33 theory Atools imports Program |
34 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml" |
34 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml" |
35 theory ProgLang imports Atools |
35 theory ProgLang imports Atools |
36 *) "ProgLang/ProgLang" |
36 *) "ProgLang/ProgLang" |
37 |
37 (* |
38 (*ML_file model.sml |
38 ML_file model.sml |
39 ML_file mstools.sml |
39 ML_file mstools.sml |
40 ML_file "specification-elems.sml" |
40 ML_file "specification-elems.sml" |
41 ML_file istate.sml |
41 ML_file istate.sml |
42 ML_file tactic.sml |
42 ML_file tactic.sml |
43 ML_file "ctree-basic.sml" (*shift to base in common with Interpret*) |
43 ML_file "ctree-basic.sml" (*shift to base in common with Interpret*) |
47 ML_file ptyps.sml |
47 ML_file ptyps.sml |
48 ML_file generate.sml |
48 ML_file generate.sml |
49 ML_file calchead.sml |
49 ML_file calchead.sml |
50 ML_file appl.sml |
50 ML_file appl.sml |
51 *) "Specify/Specify" |
51 *) "Specify/Specify" |
52 |
52 (* |
53 (*ML_file rewtools.sml |
53 ML_file rewtools.sml |
54 ML_file script.sml |
54 ML_file script.sml |
55 ML_file inform.sml |
55 ML_file inform.sml |
56 ML_file "lucas-interpreter.sml" |
56 ML_file "lucas-interpreter.sml" |
|
57 *) "Interpret/Interpret" |
|
58 (* |
57 ML_file solve.sml |
59 ML_file solve.sml |
58 ML_file mathengine.sml |
60 ML_file mathengine.sml |
59 *) "Interpret/Interpret" |
61 ML_file "~~/src/Tools/isac/Frontend/messages.sml" |
60 |
62 ML_file messages.sml |
61 (*ML_file "~~/src/Tools/isac/xmlsrc/mathml.sml" |
63 ML_file states.sml |
62 ML_file "~~/src/Tools/isac/xmlsrc/datatypes.sml" |
64 *) "MathEngine/MathEngine" |
63 ML_file "~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml" |
65 (* |
64 ML_file "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml" |
66 ML_file mathml.sml |
65 ML_file "~~/src/Tools/isac/xmlsrc/interface-xml.sml" |
67 ML_file datatypes.sml |
66 *) "xmlsrc/xmlsrc" |
68 ML_file "pbl-met-hierarchy.sml" |
67 |
69 ML_file "thy-hierarchy.sml" |
68 (*ML_file "~~/src/Tools/isac/Frontend/messages.sml" |
70 ML_file "interface-xml.sml" |
69 ML_file "~~/src/Tools/isac/Frontend/states.sml" |
71 ML_file interface.sml |
70 ML_file "~~/src/Tools/isac/Frontend/interface.sml" |
72 *) "BridgeLibisabelle/BridgeLibisabelle" |
71 |
|
72 ML_file "~~/src/Tools/isac/print_exn_G.sml" |
|
73 *) "Frontend/Frontend" |
|
74 |
73 |
75 "Knowledge/Build_Thydata" (*imports Isac.thy etc*) |
74 "Knowledge/Build_Thydata" (*imports Isac.thy etc*) |
76 |
75 |
77 (* the Protocol for the connection isac-java -- Isabelle/Isac is built separately: |
76 (* the Protocol for the connection isac-java -- Isabelle/Isac is built separately: |
78 here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *) |
77 here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *) |
96 ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close> |
95 ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close> |
97 ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close> |
96 ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close> |
98 ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close> |
97 ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close> |
99 ML \<open>Math_Engine.me; (*from "Interpret/mathengine.sml"*)\<close> |
98 ML \<open>Math_Engine.me; (*from "Interpret/mathengine.sml"*)\<close> |
100 ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close> |
99 ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close> |
101 ML \<open>print_exn_unit\<close> |
|
102 ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close> |
100 ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close> |
103 |
101 |
104 ML \<open>eval_occurs_in (*from Atools.thy*)\<close> |
102 ML \<open>eval_occurs_in (*from Atools.thy*)\<close> |
105 ML \<open>@{thm last_thmI} (*from Atools.thy*)\<close> |
103 ML \<open>@{thm last_thmI} (*from Atools.thy*)\<close> |
106 ML \<open>@{thm Querkraft_Belastung}\<close> |
104 ML \<open>@{thm Querkraft_Belastung}\<close> |