equal
deleted
inserted
replaced
12 theory Build_Isac |
12 theory Build_Isac |
13 imports |
13 imports |
14 (* structure inherited from migration which began with Isabelle2009. improve? |
14 (* structure inherited from migration which began with Isabelle2009. improve? |
15 theory KEStore |
15 theory KEStore |
16 ML_file "~~/src/Tools/isac/library.sml" |
16 ML_file "~~/src/Tools/isac/library.sml" |
|
17 ML_file "~~/src/Tools/isac/ThydataC/rule.sml" |
17 ML_file "~~/src/Tools/isac/calcelems.sml" |
18 ML_file "~~/src/Tools/isac/calcelems.sml" |
18 theory ListC |
19 theory ListC |
19 imports "~~/src/Tools/isac/KEStore" |
20 imports "~~/src/Tools/isac/KEStore" |
20 ML_file "~~/src/Tools/isac/ProgLang/termC.sml" |
21 ML_file "~~/src/Tools/isac/ProgLang/termC.sml" |
21 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml" |
22 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml" |
79 ML \<open>LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close> |
80 ML \<open>LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close> |
80 ML \<open>Math_Engine.me; (*from "Interpret/mathengine.sml"*)\<close> |
81 ML \<open>Math_Engine.me; (*from "Interpret/mathengine.sml"*)\<close> |
81 ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close> |
82 ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close> |
82 ML \<open>print_exn_unit\<close> |
83 ML \<open>print_exn_unit\<close> |
83 ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close> |
84 ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close> |
84 |
85 |
85 ML \<open>eval_occurs_in (*from Atools.thy*)\<close> |
86 ML \<open>eval_occurs_in (*from Atools.thy*)\<close> |
86 ML \<open>@{thm last_thmI} (*from Atools.thy*)\<close> |
87 ML \<open>@{thm last_thmI} (*from Atools.thy*)\<close> |
87 ML \<open>@{thm Querkraft_Belastung}\<close> |
88 ML \<open>@{thm Querkraft_Belastung}\<close> |
88 |
89 |
89 ML \<open>Celem.check_guhs_unique := false;\<close> |
90 ML \<open>Celem.check_guhs_unique := false;\<close> |