1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon May 11 11:38:52 2020 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon May 11 12:25:52 2020 +0200
     1.3 @@ -16,16 +16,26 @@
     1.4  (*  theory Know_Store imports Complex_Main
     1.5        ML_file libraryC.sml
     1.6        ML_file theoryC.sml
     1.7 -      ML_file unparseC.sml                                                                                                  
     1.8 +      ML_file unparseC.sml
     1.9        ML_file "rule-def.sml"
    1.10 -      ML_file thmC.sml
    1.11 +      ML_file "thmC-def.sml"
    1.12        ML_file "eval-def.sml"
    1.13        ML_file "rewrite-order.sml"
    1.14        ML_file rule.sml
    1.15 -      ML_file "error-fill-def.sml"
    1.16 +      ML_file "error-pattern-def.sml"
    1.17        ML_file "rule-set.sml"
    1.18 +      
    1.19 +      ML_file "store.sml"
    1.20 +      ML_file "check-unique.sml"
    1.21 +      ML_file "specification.sml"
    1.22 +      ML_file "model-pattern.sml"
    1.23 +      ML_file "problem-def.sml"
    1.24 +      ML_file "method-def.sml"
    1.25 +      ML_file "cas-def.sml"
    1.26 +      ML_file "thy-write.sml"
    1.27    theory BaseDefinitions imports Know_Store
    1.28      ML_file termC.sml
    1.29 +    ML_file substitution.sml
    1.30      ML_file contextC.sml
    1.31      ML_file environment.sml
    1.32  *)        "BaseDefinitions/BaseDefinitions"
    1.33 @@ -45,36 +55,57 @@
    1.34    theory MathEngBasic imports
    1.35      "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
    1.36      ML_file thmC.sml
    1.37 +    ML_file problem.sml
    1.38 +    ML_file method.sml
    1.39 +    ML_file "cas-command.sml"
    1.40 +  
    1.41      ML_file rewrite.sml
    1.42 +  
    1.43 +    ML_file "model-def.sml"
    1.44 +    ML_file "istate-def.sml"
    1.45      ML_file "calc-tree-elem.sml"
    1.46 -    ML_file model.sml
    1.47 -    ML_file mstools.sml
    1.48 -    ML_file "specification-elems.sml"
    1.49 -    ML_file "istate-def.sml"
    1.50 +    ML_file "pre-conds-def.sml"
    1.51 +  
    1.52      ML_file tactic.sml
    1.53 +    ML_file applicable.sml
    1.54 +  
    1.55      ML_file position.sml
    1.56      ML_file "ctree-basic.sml"
    1.57      ML_file "ctree-access.sml"
    1.58      ML_file "ctree-navi.sml"
    1.59      ML_file ctree.sml
    1.60 -  (*ML_file tactic.sml*)
    1.61 +  
    1.62 +    ML_file "state-steps.sml"
    1.63      ML_file calculation.sml
    1.64  *)        "MathEngBasic/MathEngBasic"
    1.65  (*
    1.66      theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.67    theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
    1.68 -    ML_file ptyps.sml
    1.69 -    ML_file generate.sml
    1.70 -    ML_file calchead.sml
    1.71 +    ML_file formalise.sml
    1.72 +    ML_file "o-model.sml"
    1.73 +    ML_file "i-model.sml"
    1.74 +    ML_file "p-model.sml"
    1.75 +    ML_file model.sml
    1.76 +    ML_file "pre-conditions.sml"
    1.77 +    ML_file refine.sml
    1.78 +    ML_file "mstools.sml" (*..TODO review*)
    1.79 +    ML_file ptyps.sml     (*..TODO review*)
    1.80 +    ML_file "test-out.sml"
    1.81 +    ML_file "specify-step.sml"
    1.82 +    ML_file calchead.sml  (*..TODO review*)
    1.83 +    ML_file "input-calchead.sml"
    1.84      ML_file "step-specify.sml"
    1.85      ML_file specify.sml
    1.86  *)        "Specify/Specify"
    1.87  (*
    1.88    theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
    1.89      ML_file istate.sml
    1.90 -    ML_file rewtools.sml
    1.91 +    ML_file "sub-problem.sml"
    1.92 +    ML_file "thy-read.sml"
    1.93 +    ML_file "solve-step.sml"
    1.94 +    ML_file "error-pattern.sml"
    1.95 +    ML_file derive.sml
    1.96      ML_file "li-tool.sml"
    1.97 -    ML_file inform.sml
    1.98      ML_file "lucas-interpreter.sml"
    1.99      ML_file "step-solve.sml"
   1.100  *)        "Interpret/Interpret"
   1.101 @@ -94,7 +125,8 @@
   1.102  *)        "Test_Code/Test_Code"
   1.103  (*
   1.104    theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
   1.105 -    ML_file mathml.sml
   1.106 +    ML_file "thy-present.sml"
   1.107 +    ML_file mathml.sml   
   1.108      ML_file datatypes.sml
   1.109      ML_file "pbl-met-hierarchy.sml"
   1.110      ML_file "thy-hierarchy.sml"