1.1 --- a/src/Tools/isac/Build_Isac.thy Fri Apr 16 22:13:43 2021 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Apr 16 22:29:23 2021 +0200
1.3 @@ -14,7 +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 + $ISABELLE_ISAC/BaseDefinitions
1.9 ML_file libraryC.sml
1.10 ML_file theoryC.sml
1.11 ML_file unparseC.sml
1.12 @@ -35,33 +35,33 @@
1.13 ML_file "cas-def.sml"
1.14 ML_file "thy-write.sml"
1.15 theory BaseDefinitions imports Know_Store
1.16 - ~~/src/Tools/isac/BaseDefinitions
1.17 + $ISABELLE_ISAC/BaseDefinitions
1.18 ML_file termC.sml
1.19 ML_file substitution.sml
1.20 ML_file contextC.sml
1.21 ML_file environment.sml
1.22 ( ** ) "BaseDefinitions/BaseDefinitions"( **)
1.23
1.24 -(* theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
1.25 - ~~/src/Tools/isac/ProgLang
1.26 +(* theory Calculate imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
1.27 + $ISABELLE_ISAC/ProgLang
1.28 ML_file evaluate.sml
1.29
1.30 - theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
1.31 - ~~/src/Tools/isac/ProgLang
1.32 + theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
1.33 + $ISABELLE_ISAC/ProgLang
1.34 theory Prog_Expr imports Calculate ListC
1.35 - ~~/src/Tools/isac/ProgLang
1.36 - theory Program imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
1.37 - theory Prog_Tac imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
1.38 - theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
1.39 + $ISABELLE_ISAC/ProgLang
1.40 + theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
1.41 + theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
1.42 + theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
1.43 theory Auto_Prog imports Program Prog_Tac Tactical begin
1.44 - ~~/src/Tools/isac/ProgLang
1.45 + $ISABELLE_ISAC/ProgLang
1.46 theory ProgLang imports Prog_Expr Auto_Prog
1.47 - ~~/src/Tools/isac/ProgLang
1.48 + $ISABELLE_ISAC/ProgLang
1.49 ( ** ) "ProgLang/ProgLang"( **)
1.50 (*
1.51 theory MathEngBasic imports
1.52 - "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
1.53 - ~~/src/Tools/isac/MathEngBasic
1.54 + "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
1.55 + $ISABELLE_ISAC/MathEngBasic
1.56 ML_file thmC.sml
1.57 ML_file problem.sml
1.58 ML_file method.sml
1.59 @@ -87,10 +87,10 @@
1.60 ML_file calculation.sml
1.61 ( ** ) "MathEngBasic/MathEngBasic"( **)
1.62 (*
1.63 - theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
1.64 - ~~/src/Tools/isac/Specify
1.65 - theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
1.66 - ~~/src/Tools/isac/Specify
1.67 + theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
1.68 + $ISABELLE_ISAC/Specify
1.69 + theory Specify imports "$ISABELLE_ISAC/ProgLang/ProgLang" Input_Descript
1.70 + $ISABELLE_ISAC/Specify
1.71 ML_file formalise.sml
1.72 ML_file "o-model.sml"
1.73 ML_file "i-model.sml"
1.74 @@ -108,8 +108,8 @@
1.75 ML_file specify.sml
1.76 ( ** ) "Specify/Specify"( **)
1.77 (*
1.78 - theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
1.79 - ~~/src/Tools/isac/Interpret
1.80 + theory Interpret imports "$ISABELLE_ISAC/Specify/Specify"
1.81 + $ISABELLE_ISAC/Interpret
1.82 ML_file istate.sml
1.83 ML_file "sub-problem.sml"
1.84 ML_file "thy-read.sml"
1.85 @@ -122,7 +122,7 @@
1.86 ( ** ) "Interpret/Interpret"( **)
1.87 (*
1.88 theory MathEngine imports Interpret.Interpret
1.89 - ~~/src/Tools/isac/MathEngine
1.90 + $ISABELLE_ISAC/MathEngine
1.91 ML_file "fetch-tactics.sml"
1.92 ML_file solve.sml
1.93 ML_file step.sml
1.94 @@ -132,13 +132,13 @@
1.95 ML_file states.sml
1.96 ( ** ) "MathEngine/MathEngine"( **)
1.97 (*
1.98 - theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
1.99 - ~~/src/Tools/isac/Test_Code
1.100 + theory Test_Code imports "$ISABELLE_ISAC/MathEngine/MathEngine"
1.101 + $ISABELLE_ISAC/Test_Code
1.102 ML_file "test-code.sml"
1.103 ( ** ) "Test_Code/Test_Code"( **)
1.104 (*
1.105 - theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
1.106 - ~~/src/Tools/isac/BridgeLibisabelle
1.107 + theory BridgeLibisabelle imports "$ISABELLE_ISAC/MathEngine/MathEngine"
1.108 + $ISABELLE_ISAC/BridgeLibisabelle
1.109 ML_file "thy-present.sml"
1.110 ML_file mathml.sml
1.111 ML_file datatypes.sml
1.112 @@ -149,14 +149,14 @@
1.113 ( ** ) "BridgeLibisabelle/BridgeLibisabelle"( **)
1.114 (*
1.115 theory Calculation imports Calculation (*preliminary for starting Isabelle/Isac*)
1.116 - ~~/src/Tools/isac/BridgeJEdit
1.117 + $ISABELLE_ISAC/BridgeJEdit
1.118 ML_file parseC.sml
1.119 ML_file preliminary.sml
1.120 theory BridgeJEdit imports Calculation (*preliminary for starting Isabelle/Isac*)
1.121 - ~~/src/Tools/isac/BridgeJEdit
1.122 + $ISABELLE_ISAC/BridgeJEdit
1.123 ( ** ) "BridgeLibisabelle/BridgeLibisabelle"( **)
1.124 (*
1.125 - theory Isac imports "~~/src/Tools/isac/MathEngine/MathEngine"
1.126 + theory Isac imports "$ISABELLE_ISAC/MathEngine/MathEngine"
1.127 ML_file parseC.sml
1.128 theory BridgeJEdit imports Isac
1.129 ( **) "BridgeJEdit/BridgeJEdit" (*DEactivate after devel.of BridgeJEdit*)
1.130 @@ -228,7 +228,7 @@
1.131 unsatisfactory with respect to logical soundness.
1.132 Since Isabelle now has started to care about floating point numbers, it is high
1.133 time to adopt these together with the other numerals. Isabelle2012/13's numerals
1.134 - are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".
1.135 + are different from Isabelle2011, see "$ISABELLE_ISAC_TEST/ProgLang/termC.sml".
1.136
1.137 The transition from "Free" to standard numerals is a task to be scheduled for
1.138 several weeks. The urgency of this task follows from the experience,