src/Tools/isac/Build_Isac.thy
changeset 59814 665dd868d4e2
parent 59801 17d807bf28fb
child 59833 9331e61f55dd
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Feb 21 14:19:33 2020 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Feb 24 17:51:26 2020 +0100
     1.3 @@ -80,6 +80,10 @@
     1.4      ML_file states.sml
     1.5  *)        "MathEngine/MathEngine"
     1.6  (*
     1.7 +  theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
     1.8 +    ML_file "test-code.sml"
     1.9 +*)        "Test_Code/Test_Code"
    1.10 +(*
    1.11    theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
    1.12      ML_file mathml.sml
    1.13      ML_file datatypes.sml
    1.14 @@ -114,7 +118,7 @@
    1.15  ML \<open>Num_Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
    1.16  ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
    1.17  ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
    1.18 -ML \<open>Math_Engine.me;\<close>
    1.19 +ML \<open>Test_Code.me;\<close>
    1.20  text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
    1.21  ML \<open>prog_expr\<close>
    1.22