diff -r bfabbaf915b1 -r 3da177a07c3e src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Fri Oct 25 16:07:15 2019 +0200 +++ b/src/Tools/isac/Build_Isac.thy Sat Oct 26 13:03:16 2019 +0200 @@ -34,17 +34,22 @@ ML_file rewrite.sml *) "ProgLang/ProgLang" (* - theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements" - theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript + theory MathEngBasic imports + "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript" + ML_file "calc-tree-elem.sml" ML_file model.sml ML_file mstools.sml ML_file "specification-elems.sml" ML_file istate.sml ML_file tactic.sml - ML_file "ctree-basic.sml" (*shift to base in common with Interpret*) - ML_file "ctree-access.sml"(*shift to base in common with Interpret*) - ML_file "ctree-navi.sml" (*shift to base in common with Interpret*) - ML_file ctree.sml (*shift to base in common with Interpret*) + ML_file "ctree-basic.sml" + ML_file "ctree-access.sml" + ML_file "ctree-navi.sml" + ML_file ctree.sml +*) "MathEngBasic/MathEngBasic" +(* + theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements" + theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript ML_file ptyps.sml ML_file generate.sml ML_file calchead.sml