src/Tools/isac/Build_Isac.thy
changeset 59865 75a9d629ea53
parent 59858 a2c32a38327a
child 59866 3b194392ea71
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Apr 10 12:28:47 2020 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Fri Apr 10 14:46:55 2020 +0200
     1.3 @@ -15,12 +15,13 @@
     1.4  imports
     1.5  (*  theory KEStore imports Complex_Main
     1.6        ML_file libraryC.sml
     1.7 +      ML_file theoryC.sml
     1.8 +      ML_file unparseC.sml
     1.9        ML_file "rule-def.sml"
    1.10 +      ML_file thmC.sml
    1.11        ML_file "exec-def.sml"
    1.12        ML_file "rewrite-order.sml"
    1.13 -      ML_file theoryC.sml
    1.14        ML_file rule.sml
    1.15 -      ML_file thmC.sml
    1.16        ML_file "error-fill-def.sml"
    1.17        ML_file "rule-set.sml"
    1.18        ML_file calcelems.sml
    1.19 @@ -40,11 +41,11 @@
    1.20        theory Tactical imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.21      theory Auto_Prog imports Program Prog_Tac Tactical begin
    1.22    theory ProgLang imports Prog_Expr Auto_Prog
    1.23 -    ML_file rewrite.sml
    1.24  *)        "ProgLang/ProgLang"
    1.25  (*
    1.26    theory MathEngBasic imports
    1.27      "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
    1.28 +    ML_file rewrite.sml
    1.29      ML_file "calc-tree-elem.sml"
    1.30      ML_file model.sml
    1.31      ML_file mstools.sml