1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Mar 22 17:22:08 2021 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sat Apr 03 15:27:52 2021 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  theory Build_Isac
     1.5  imports
     1.6  (*  theory Know_Store imports Complex_Main
     1.7 +    ~~/src/Tools/isac/BaseDefinitions
     1.8        ML_file libraryC.sml
     1.9        ML_file theoryC.sml
    1.10        ML_file unparseC.sml
    1.11 @@ -34,6 +35,7 @@
    1.12        ML_file "cas-def.sml"
    1.13        ML_file "thy-write.sml"
    1.14    theory BaseDefinitions imports Know_Store
    1.15 +  ~~/src/Tools/isac/BaseDefinitions
    1.16      ML_file termC.sml
    1.17      ML_file substitution.sml
    1.18      ML_file contextC.sml
    1.19 @@ -41,19 +43,25 @@
    1.20  ( ** )    "BaseDefinitions/BaseDefinitions"( **)
    1.21  
    1.22  (*    theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.23 +      ~~/src/Tools/isac/ProgLang
    1.24          ML_file evaluate.sml
    1.25  
    1.26        theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.27 +      ~~/src/Tools/isac/ProgLang
    1.28      theory Prog_Expr imports Calculate ListC
    1.29 +    ~~/src/Tools/isac/ProgLang
    1.30        theory Program imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.31        theory Prog_Tac imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.32        theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.33      theory Auto_Prog imports Program Prog_Tac Tactical begin
    1.34 +    ~~/src/Tools/isac/ProgLang
    1.35    theory ProgLang imports Prog_Expr Auto_Prog
    1.36 +  ~~/src/Tools/isac/ProgLang
    1.37  ( ** )    "ProgLang/ProgLang"( **)
    1.38  (*
    1.39    theory MathEngBasic imports
    1.40      "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
    1.41 +  ~~/src/Tools/isac/MathEngBasic
    1.42      ML_file thmC.sml
    1.43      ML_file problem.sml
    1.44      ML_file method.sml
    1.45 @@ -80,7 +88,9 @@
    1.46  ( ** )    "MathEngBasic/MathEngBasic"( **)
    1.47  (*
    1.48      theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.49 +    ~~/src/Tools/isac/Specify
    1.50    theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
    1.51 +  ~~/src/Tools/isac/Specify
    1.52      ML_file formalise.sml
    1.53      ML_file "o-model.sml"
    1.54      ML_file "i-model.sml"
    1.55 @@ -99,6 +109,7 @@
    1.56  ( ** )    "Specify/Specify"( **)
    1.57  (*
    1.58    theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
    1.59 +  ~~/src/Tools/isac/Interpret
    1.60      ML_file istate.sml
    1.61      ML_file "sub-problem.sml"
    1.62      ML_file "thy-read.sml"
    1.63 @@ -111,6 +122,7 @@
    1.64  ( ** )    "Interpret/Interpret"( **)
    1.65  (*
    1.66    theory MathEngine imports Interpret.Interpret
    1.67 +  ~~/src/Tools/isac/MathEngine
    1.68      ML_file "fetch-tactics.sml"
    1.69      ML_file solve.sml
    1.70      ML_file step.sml
    1.71 @@ -121,10 +133,12 @@
    1.72  ( ** )    "MathEngine/MathEngine"( **)
    1.73  (*
    1.74    theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
    1.75 +  ~~/src/Tools/isac/Test_Code
    1.76      ML_file "test-code.sml"
    1.77  ( ** )    "Test_Code/Test_Code"( **)
    1.78  (*
    1.79    theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
    1.80 +  ~~/src/Tools/isac/BridgeLibisabelle
    1.81      ML_file "thy-present.sml"
    1.82      ML_file mathml.sml   
    1.83      ML_file datatypes.sml
    1.84 @@ -134,6 +148,14 @@
    1.85      ML_file interface.sml
    1.86  ( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)
    1.87  (*
    1.88 +    theory Calculation imports Calculation (*preliminary for starting Isabelle/Isac*)
    1.89 +    ~~/src/Tools/isac/BridgeJEdit
    1.90 +      ML_file parseC.sml
    1.91 +      ML_file preliminary.sml
    1.92 +  theory BridgeJEdit imports Calculation (*preliminary for starting Isabelle/Isac*)
    1.93 +  ~~/src/Tools/isac/BridgeJEdit
    1.94 +( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)
    1.95 +(*
    1.96      theory Isac imports  "~~/src/Tools/isac/MathEngine/MathEngine"
    1.97        ML_file parseC.sml
    1.98    theory BridgeJEdit imports Isac