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