1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Apr 16 22:13:43 2021 +0200
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Apr 16 22:29:23 2021 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  theory Calculation
     1.6  imports
     1.7 -(**)"~~/src/Tools/isac/Knowledge/Build_Thydata"   (*remove after devel.of BridgeJEdit*)
     1.8 -(**)"~~/src/Tools/isac/MathEngine/MathEngine"
     1.9 +(**)"$ISABELLE_ISAC/Knowledge/Build_Thydata"   (*remove after devel.of BridgeJEdit*)
    1.10 +(**)"$ISABELLE_ISAC/MathEngine/MathEngine"
    1.11  (**)"HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)
    1.12  keywords
    1.13    "Example" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*)

     2.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Fri Apr 16 22:13:43 2021 +0200
     2.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Fri Apr 16 22:29:23 2021 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  *)
     2.5  
     2.6  theory BridgeLibisabelle
     2.7 -  imports "~~/src/Tools/isac/Test_Code/Test_Code"
     2.8 +  imports "$ISABELLE_ISAC/Test_Code/Test_Code"
     2.9  begin
    2.10    ML_file "present-tool.sml"
    2.11    ML_file "thy-present.sml"

     3.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Apr 16 22:13:43 2021 +0200
     3.2 +++ b/src/Tools/isac/Build_Isac.thy	Fri Apr 16 22:29:23 2021 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4  theory Build_Isac
     3.5  imports
     3.6  (*  theory Know_Store imports Complex_Main
     3.7 -    ~~/src/Tools/isac/BaseDefinitions
     3.8 +    $ISABELLE_ISAC/BaseDefinitions
     3.9        ML_file libraryC.sml
    3.10        ML_file theoryC.sml
    3.11        ML_file unparseC.sml
    3.12 @@ -35,33 +35,33 @@
    3.13        ML_file "cas-def.sml"
    3.14        ML_file "thy-write.sml"
    3.15    theory BaseDefinitions imports Know_Store
    3.16 -  ~~/src/Tools/isac/BaseDefinitions
    3.17 +  $ISABELLE_ISAC/BaseDefinitions
    3.18      ML_file termC.sml
    3.19      ML_file substitution.sml
    3.20      ML_file contextC.sml
    3.21      ML_file environment.sml
    3.22  ( ** )    "BaseDefinitions/BaseDefinitions"( **)
    3.23  
    3.24 -(*    theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    3.25 -      ~~/src/Tools/isac/ProgLang
    3.26 +(*    theory Calculate imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    3.27 +      $ISABELLE_ISAC/ProgLang
    3.28          ML_file evaluate.sml
    3.29  
    3.30 -      theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    3.31 -      ~~/src/Tools/isac/ProgLang
    3.32 +      theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    3.33 +      $ISABELLE_ISAC/ProgLang
    3.34      theory Prog_Expr imports Calculate ListC
    3.35 -    ~~/src/Tools/isac/ProgLang
    3.36 -      theory Program imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    3.37 -      theory Prog_Tac imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    3.38 -      theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    3.39 +    $ISABELLE_ISAC/ProgLang
    3.40 +      theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    3.41 +      theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    3.42 +      theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    3.43      theory Auto_Prog imports Program Prog_Tac Tactical begin
    3.44 -    ~~/src/Tools/isac/ProgLang
    3.45 +    $ISABELLE_ISAC/ProgLang
    3.46    theory ProgLang imports Prog_Expr Auto_Prog
    3.47 -  ~~/src/Tools/isac/ProgLang
    3.48 +  $ISABELLE_ISAC/ProgLang
    3.49  ( ** )    "ProgLang/ProgLang"( **)
    3.50  (*
    3.51    theory MathEngBasic imports
    3.52 -    "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
    3.53 -  ~~/src/Tools/isac/MathEngBasic
    3.54 +    "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
    3.55 +  $ISABELLE_ISAC/MathEngBasic
    3.56      ML_file thmC.sml
    3.57      ML_file problem.sml
    3.58      ML_file method.sml
    3.59 @@ -87,10 +87,10 @@
    3.60      ML_file calculation.sml
    3.61  ( ** )    "MathEngBasic/MathEngBasic"( **)
    3.62  (*
    3.63 -    theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    3.64 -    ~~/src/Tools/isac/Specify
    3.65 -  theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
    3.66 -  ~~/src/Tools/isac/Specify
    3.67 +    theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    3.68 +    $ISABELLE_ISAC/Specify
    3.69 +  theory Specify imports "$ISABELLE_ISAC/ProgLang/ProgLang" Input_Descript
    3.70 +  $ISABELLE_ISAC/Specify
    3.71      ML_file formalise.sml
    3.72      ML_file "o-model.sml"
    3.73      ML_file "i-model.sml"
    3.74 @@ -108,8 +108,8 @@
    3.75      ML_file specify.sml
    3.76  ( ** )    "Specify/Specify"( **)
    3.77  (*
    3.78 -  theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
    3.79 -  ~~/src/Tools/isac/Interpret
    3.80 +  theory Interpret imports "$ISABELLE_ISAC/Specify/Specify"
    3.81 +  $ISABELLE_ISAC/Interpret
    3.82      ML_file istate.sml
    3.83      ML_file "sub-problem.sml"
    3.84      ML_file "thy-read.sml"
    3.85 @@ -122,7 +122,7 @@
    3.86  ( ** )    "Interpret/Interpret"( **)
    3.87  (*
    3.88    theory MathEngine imports Interpret.Interpret
    3.89 -  ~~/src/Tools/isac/MathEngine
    3.90 +  $ISABELLE_ISAC/MathEngine
    3.91      ML_file "fetch-tactics.sml"
    3.92      ML_file solve.sml
    3.93      ML_file step.sml
    3.94 @@ -132,13 +132,13 @@
    3.95      ML_file states.sml
    3.96  ( ** )    "MathEngine/MathEngine"( **)
    3.97  (*
    3.98 -  theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
    3.99 -  ~~/src/Tools/isac/Test_Code
   3.100 +  theory Test_Code imports "$ISABELLE_ISAC/MathEngine/MathEngine"
   3.101 +  $ISABELLE_ISAC/Test_Code
   3.102      ML_file "test-code.sml"
   3.103  ( ** )    "Test_Code/Test_Code"( **)
   3.104  (*
   3.105 -  theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
   3.106 -  ~~/src/Tools/isac/BridgeLibisabelle
   3.107 +  theory BridgeLibisabelle imports "$ISABELLE_ISAC/MathEngine/MathEngine"
   3.108 +  $ISABELLE_ISAC/BridgeLibisabelle
   3.109      ML_file "thy-present.sml"
   3.110      ML_file mathml.sml   
   3.111      ML_file datatypes.sml
   3.112 @@ -149,14 +149,14 @@
   3.113  ( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)
   3.114  (*
   3.115      theory Calculation imports Calculation (*preliminary for starting Isabelle/Isac*)
   3.116 -    ~~/src/Tools/isac/BridgeJEdit
   3.117 +    $ISABELLE_ISAC/BridgeJEdit
   3.118        ML_file parseC.sml
   3.119        ML_file preliminary.sml
   3.120    theory BridgeJEdit imports Calculation (*preliminary for starting Isabelle/Isac*)
   3.121 -  ~~/src/Tools/isac/BridgeJEdit
   3.122 +  $ISABELLE_ISAC/BridgeJEdit
   3.123  ( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)
   3.124  (*
   3.125 -    theory Isac imports  "~~/src/Tools/isac/MathEngine/MathEngine"
   3.126 +    theory Isac imports  "$ISABELLE_ISAC/MathEngine/MathEngine"
   3.127        ML_file parseC.sml
   3.128    theory BridgeJEdit imports Isac    
   3.129  ( **)    "BridgeJEdit/BridgeJEdit"  (*DEactivate after devel.of BridgeJEdit*)
   3.130 @@ -228,7 +228,7 @@
   3.131    unsatisfactory with respect to logical soundness.
   3.132    Since Isabelle now has started to care about floating point numbers, it is high 
   3.133    time to adopt these together with the other numerals. Isabelle2012/13's numerals
   3.134 -  are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".
   3.135 +  are different from Isabelle2011, see "$ISABELLE_ISAC_TEST/ProgLang/termC.sml".
   3.136    
   3.137    The transition from "Free" to standard numerals is a task to be scheduled for 
   3.138    several weeks. The urgency of this task follows from the experience, 

     4.1 --- a/src/Tools/isac/Isac_Protocol.thy	Fri Apr 16 22:13:43 2021 +0200
     4.2 +++ b/src/Tools/isac/Isac_Protocol.thy	Fri Apr 16 22:29:23 2021 +0200
     4.3 @@ -1,5 +1,5 @@
     4.4  theory Isac_Protocol
     4.5 -imports "~~/src/Tools/isac/Knowledge/Build_Thydata" Protocol.Protocol
     4.6 +imports "$ISABELLE_ISAC/Knowledge/Build_Thydata" Protocol.Protocol
     4.7  begin
     4.8  
     4.9  (* val appendFormula : calcID -> cterm' -> XML.tree *)

     5.1 --- a/src/Tools/isac/Knowledge/Isac_Knowledge.thy	Fri Apr 16 22:13:43 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/Isac_Knowledge.thy	Fri Apr 16 22:29:23 2021 +0200
     5.3 @@ -4,8 +4,8 @@
     5.4  
     5.5  theory Isac_Knowledge
     5.6  imports
     5.7 -(**) "~~/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle" (*remove after devel.of BridgeJEdit*)
     5.8 -(** )"~~/src/Tools/isac/BridgeJEdit/BridgeJEdit"          ( *activate after devel.of BridgeJEdit*)
     5.9 +(**) "$ISABELLE_ISAC/BridgeLibisabelle/BridgeLibisabelle" (*remove after devel.of BridgeJEdit*)
    5.10 +(** )"$ISABELLE_ISAC/BridgeJEdit/BridgeJEdit"          ( *activate after devel.of BridgeJEdit*)
    5.11    PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin InsSort
    5.12    DiophantEq Inverse_Z_Transform Test
    5.13  begin

     6.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Fri Apr 16 22:13:43 2021 +0200
     6.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Fri Apr 16 22:29:23 2021 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  Defitions required for both, for Specify and for the Lucas-Interpreter.
     6.5  *)
     6.6  theory MathEngBasic
     6.7 -imports "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
     6.8 +imports "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
     6.9  begin
    6.10  (* removed all warnings here, only "handle _" remains *)
    6.11    ML_file thmC.sml

     7.1 --- a/src/Tools/isac/ProgLang/Calculate.thy	Fri Apr 16 22:13:43 2021 +0200
     7.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy	Fri Apr 16 22:29:23 2021 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  *)
     7.5  
     7.6  theory Calculate
     7.7 -  imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
     7.8 +  imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
     7.9  begin
    7.10  
    7.11  text \<open>Abstract:

     8.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Fri Apr 16 22:13:43 2021 +0200
     8.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Fri Apr 16 22:29:23 2021 +0200
     8.3 @@ -3,7 +3,7 @@
     8.4     (c) due to copyright terms
     8.5  *)
     8.6  
     8.7 -theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
     8.8 +theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
     8.9  
    8.10  begin
    8.11  

     9.1 --- a/src/Tools/isac/ProgLang/Program.thy	Fri Apr 16 22:13:43 2021 +0200
     9.2 +++ b/src/Tools/isac/ProgLang/Program.thy	Fri Apr 16 22:29:23 2021 +0200
     9.3 @@ -4,7 +4,7 @@
     9.4  *)
     9.5  
     9.6  theory Program
     9.7 -  imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
     9.8 +  imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
     9.9  begin
    9.10  
    9.11  text \<open>Abstract:

    10.1 --- a/src/Tools/isac/ProgLang/Tactical.thy	Fri Apr 16 22:13:43 2021 +0200
    10.2 +++ b/src/Tools/isac/ProgLang/Tactical.thy	Fri Apr 16 22:29:23 2021 +0200
    10.3 @@ -3,7 +3,7 @@
    10.4     (c) due to copyright terms
    10.5   *)
    10.6  theory Tactical
    10.7 -  imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    10.8 +  imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    10.9  begin
   10.10  
   10.11  text \<open>Abstract:

    11.1 --- a/src/Tools/isac/Specify/Input_Descript.thy	Fri Apr 16 22:13:43 2021 +0200
    11.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy	Fri Apr 16 22:29:23 2021 +0200
    11.3 @@ -7,7 +7,7 @@
    11.4  the types of the descriptors below can be more relaxed. 
    11.5  *)
    11.6  
    11.7 -theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    11.8 +theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    11.9  begin
   11.10  
   11.11  subsection \<open>typedecl for descriptors of input in specify-phase\<close>

    12.1 --- a/src/Tools/isac/Specify/Specify.thy	Fri Apr 16 22:13:43 2021 +0200
    12.2 +++ b/src/Tools/isac/Specify/Specify.thy	Fri Apr 16 22:29:23 2021 +0200
    12.3 @@ -4,7 +4,7 @@
    12.4   *)
    12.5  
    12.6  theory Specify
    12.7 -imports "~~/src/Tools/isac/MathEngBasic/MathEngBasic"
    12.8 +imports "$ISABELLE_ISAC/MathEngBasic/MathEngBasic"
    12.9  begin
   12.10  (* removed all warnings here, only "handle _" remains *)
   12.11    ML_file formalise.sml

    13.1 --- a/src/Tools/isac/TODO.thy	Fri Apr 16 22:13:43 2021 +0200
    13.2 +++ b/src/Tools/isac/TODO.thy	Fri Apr 16 22:29:23 2021 +0200
    13.3 @@ -326,7 +326,7 @@
    13.4  text \<open>
    13.5    \begin{itemize}
    13.6    \item there are comments in several signatures
    13.7 -  \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
    13.8 +  \item ML_file "$ISABELLE_ISAC/Interpret/specification-elems.sml" can be (almost) deleted
    13.9    \item src/../Frontend/: signatures missing
   13.10    \item xxx
   13.11    \end{itemize}
   13.12 @@ -337,7 +337,7 @@
   13.13    \item try to separate Isac_Knowledge from MathEngine
   13.14      common base: Knowledge_Author / ..??
   13.15    \item xxx
   13.16 -  \item  ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
   13.17 +  \item  ML_file "$ISABELLE_ISAC/Interpret/ctree.sml" (*shift to base in common with Interpret*)
   13.18    \item xxx
   13.19    \item xxx
   13.20    \item xxx

    14.1 --- a/src/Tools/isac/Test_Code/Test_Code.thy	Fri Apr 16 22:13:43 2021 +0200
    14.2 +++ b/src/Tools/isac/Test_Code/Test_Code.thy	Fri Apr 16 22:29:23 2021 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  *)
    14.5  
    14.6  theory Test_Code
    14.7 -imports "~~/src/Tools/isac/MathEngine/MathEngine"
    14.8 +imports "$ISABELLE_ISAC/MathEngine/MathEngine"
    14.9  begin
   14.10  
   14.11    ML_file "test-code.sml"

    15.1 --- a/src/Tools/isac/Test_Code/test-code.sml	Fri Apr 16 22:13:43 2021 +0200
    15.2 +++ b/src/Tools/isac/Test_Code/test-code.sml	Fri Apr 16 22:29:23 2021 +0200
    15.3 @@ -1,7 +1,7 @@
    15.4 -(*  Title:      ~~/test/../Testcode/test-code.sml
    15.5 +(*  Title:      Tools/isac/Testcode/test-code.sml
    15.6      Author:     Walther Neuper 200222
    15.7  
    15.8 -Code used ONLY for ~~/test/*
    15.9 +Code used ONLY for $ISABELLE_ISAC_TEST/*
   15.10  *)
   15.11  
   15.12  signature TEST_CODE =

    16.1 --- a/test/Pure/library_scala.thy	Fri Apr 16 22:13:43 2021 +0200
    16.2 +++ b/test/Pure/library_scala.thy	Fri Apr 16 22:29:23 2021 +0200
    16.3 @@ -11,7 +11,7 @@
    16.4        3-fold implementation of insertion sort, in
    16.5        # SML: below
    16.6        # Scala: below, evaluate in jEdit > Console > Scala
    16.7 -      # Isabelle: ~~~/src/Tools/isac/Knowledge/InsSort.thy by rewriting
    16.8 +      # Isabelle: ~$ISABELLE_ISAC/Knowledge/InsSort.thy by rewriting
    16.9  \<close>
   16.10  
   16.11  ML \<open>

    17.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy	Fri Apr 16 22:13:43 2021 +0200
    17.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy	Fri Apr 16 22:29:23 2021 +0200
    17.3 @@ -3,7 +3,7 @@
    17.4     (c) due to copyright terms
    17.5  
    17.6    this theory is evaluated BEFORE Test_Isac.thy opens structures.
    17.7 -  So, if you encounter errors here, first fix them in ~~/test/Tools/isac/Minimsubpbl/* *)
    17.8 +  So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Minimsubpbl/* *)
    17.9  
   17.10  theory All_Ctxt imports Isac.Build_Isac
   17.11  begin

    18.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Fri Apr 16 22:13:43 2021 +0200
    18.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Fri Apr 16 22:29:23 2021 +0200
    18.3 @@ -19,7 +19,7 @@
    18.4    ISAC tutoring system ! ISAC finds the rules automatically. Here we start by 
    18.5    telling the rules ourselves.
    18.6    Let's differentiate after we have identified the rules for differentiation, as 
    18.7 -  found in ~~/src/Tools/isac/Knowledge/Diff.thy:
    18.8 +  found in $ISABELLE_ISAC/Knowledge/Diff.thy:
    18.9  \<close>
   18.10  ML \<open>
   18.11  val diff_sum = ThmC.numerals_to_Free @{thm diff_sum};
   18.12 @@ -181,7 +181,7 @@
   18.13    in all intermediate steps.
   18.14  
   18.15    So we started to develop (in German !) such a simplifier in 
   18.16 -  ~~/src/Tools/isac/Knowledge/PolyMinus.thy
   18.17 +  $ISABELLE_ISAC/Knowledge/PolyMinus.thy
   18.18  \<close>
   18.19  
   18.20  subsection \<open>What already works\<close>

    19.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Fri Apr 16 22:13:43 2021 +0200
    19.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Fri Apr 16 22:29:23 2021 +0200
    19.3 @@ -24,7 +24,7 @@
    19.4    specification of the problem and (3) a method solving the problem.
    19.5  
    19.6    ad (1) The rules required for simplifying our example are found in theory
    19.7 -  ~~/Tools/isac/Knowledge/PolyMinus.thy. 
    19.8 +  $ISABELLE_ISAC/Knowledge/PolyMinus.thy. 
    19.9  
   19.10    ad (2) The problem of 'vereinfachen' is one of many other problems;
   19.11    the function 'get_pbt' gets the one we need:  
   19.12 @@ -46,7 +46,7 @@
   19.13  MethodC.from_store ["simplification", "for_polynomials", "with_minus"];
   19.14  \<close>
   19.15  text \<open>For a readable format of the method look up the definition in
   19.16 -  ~~/Tools/isac/Knowledge/PolyMinus.thy or 
   19.17 +  $ISABELLE_ISAC/Knowledge/PolyMinus.thy or 
   19.18    http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html
   19.19    The path to the method "simplification - for_polynomials - with_minus" is
   19.20    not reversed like the one to the problem, because the structure of the

    20.1 --- a/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test.thy	Fri Apr 16 22:13:43 2021 +0200
    20.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test.thy	Fri Apr 16 22:29:23 2021 +0200
    20.3 @@ -21,14 +21,14 @@
    20.4                      {..., Nitpick, Main, testdir1, testdirm, Build_Test}*)
    20.5  imports 
    20.6    Complex_Main 
    20.7 -  "~~/test/Tools/isac/ADDTESTS/file-depend/1language/Foo_Language" 
    20.8 -  "~~/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_KnowALL"
    20.9 +  "$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/1language/Foo_Language" 
   20.10 +  "$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/3knowledge/Foo_KnowALL"
   20.11  begin
   20.12 -  ML_file "~~/test/Tools/isac/ADDTESTS/file-depend/0foolibrary.ML"                    
   20.13 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/0foolibrary.ML"                    
   20.14      ML \<open>val Free ("b", _) = foolibrhs  @{term "a = b"}\<close>
   20.15  (*use_thy "1language/Foo_Language" --- is done by import above*)        
   20.16      ML \<open>val Const ("Foo_Language.fooprog", _) = @{term fooprog}\<close>
   20.17 -  ML_file "~~/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML"   
   20.18 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML"   
   20.19      ML \<open>val Free ("b", _) = foointerpret @{term "fooprog (a = b)"}\<close>
   20.20  
   20.21  text \<open>the different theories of knowledge are recognized, Const bar*:\<close>

    21.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml	Fri Apr 16 22:13:43 2021 +0200
    21.2 +++ b/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml	Fri Apr 16 22:29:23 2021 +0200
    21.3 @@ -5,7 +5,7 @@
    21.4  theory Test_Some imports Isac.Build_Thydata begin 
    21.5  ML {* KEStore_Elems.set_ref_thy @{theory};
    21.6    fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
    21.7 -ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
    21.8 +ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml"
    21.9  *)
   21.10  
   21.11  (* NOTE: Protocol.thy still belongs to a different development at

    22.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Fri Apr 16 22:13:43 2021 +0200
    22.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Fri Apr 16 22:29:23 2021 +0200
    22.3 @@ -3,7 +3,7 @@
    22.4     (c) due to copyright terms
    22.5  
    22.6  theory Test_Some imports Isac.Build_Thydata begin 
    22.7 -ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
    22.8 +ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/lucas_interpreter.sml"
    22.9  ML_file "xmlsrc/thy-hierarchy.sml"
   22.10  
   22.11  CAUTION with testing *2file functions -- they are actually writing to ~/tmp

    23.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml	Fri Apr 16 22:13:43 2021 +0200
    23.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml	Fri Apr 16 22:29:23 2021 +0200
    23.3 @@ -3,7 +3,7 @@
    23.4      (c) due to copyright terms
    23.5  
    23.6  theory Test_Some imports Isac.Build_Isac begin 
    23.7 -ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
    23.8 +ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/lucas_interpreter.sml"
    23.9  ML_file "Knowledge/build_thydata.sml"
   23.10  *)
   23.11  
   23.12 @@ -32,8 +32,8 @@
   23.13    such, that it hangs (probably due to some full buffer)
   23.14    test below compiled with
   23.15  theory Test_Theory
   23.16 -imports "~~/src/Tools/isac/Knowledge/Isac" "~~/src/Tools/isac/Interpret/Interpret"
   23.17 -  "~~/src/Tools/isac/Knowledge/Test_Build_Thydata"
   23.18 +imports "$ISABELLE_ISAC/Knowledge/Isac" "$ISABELLE_ISAC/Interpret/Interpret"
   23.19 +  "$ISABELLE_ISAC/Knowledge/Test_Build_Thydata"
   23.20  begin                                                                            
   23.21  *)
   23.22  (*/----- cp from Build_Thydata.thy -----------------------------------------------------------\*)

    24.1 --- a/test/Tools/isac/Knowledge/gcd_poly.thy	Fri Apr 16 22:13:43 2021 +0200
    24.2 +++ b/test/Tools/isac/Knowledge/gcd_poly.thy	Fri Apr 16 22:29:23 2021 +0200
    24.3 @@ -1,5 +1,5 @@
    24.4  theory gcd_poly 
    24.5 -imports (*"~~/src/Tools/isac/Knowledge/GCD_Poly"*) Isac.Isac_Knowledge
    24.6 +imports (*"$ISABELLE_ISAC/Knowledge/GCD_Poly"*) Isac.Isac_Knowledge
    24.7  begin
    24.8  
    24.9  (*here come the tests from GCD_Poly.thy*)

    25.1 --- a/test/Tools/isac/Knowledge/gcd_poly_winkler.sml	Fri Apr 16 22:13:43 2021 +0200
    25.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_winkler.sml	Fri Apr 16 22:29:23 2021 +0200
    25.3 @@ -6,8 +6,8 @@
    25.4  
    25.5  Programcode according to [1] for later lookup for mathematicians.
    25.6  The tests below remain according to [1], 
    25.7 -while "~~/test/Tools/isac/Knowledge/gcd_poly.sml" start exactly from the same state
    25.8 -and in time follows development in "~~/src/Tools/isac/Knowledge/GCD_Poly.thy".
    25.9 +while "$ISABELLE_ISAC_TEST/Knowledge/gcd_poly.sml" start exactly from the same state
   25.10 +and in time follows development in "$ISABELLE_ISAC/Knowledge/GCD_Poly.thy".
   25.11  
   25.12  [1] Franz Winkler. Polynomial Algorithms in Computer Algebra.
   25.13  Springer-Verlag/Wien 1996.

    26.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Apr 16 22:13:43 2021 +0200
    26.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Apr 16 22:29:23 2021 +0200
    26.3 @@ -5,7 +5,7 @@
    26.4  theory Test_Some imports Build_Thydata begin 
    26.5  ML {* KEStore_Elems.set_ref_thy @{theory};
    26.6    fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
    26.7 -ML_file "~~/test/Tools/isac/Interpret/mathengine.sml"
    26.8 +ML_file "$ISABELLE_ISAC_TEST/Interpret/mathengine.sml"
    26.9  *)
   26.10  "--------------------------------------------------------";
   26.11  "table of contents --------------------------------------";

    27.1 --- a/test/Tools/isac/Specify/refine.thy	Fri Apr 16 22:13:43 2021 +0200
    27.2 +++ b/test/Tools/isac/Specify/refine.thy	Fri Apr 16 22:29:23 2021 +0200
    27.3 @@ -43,7 +43,7 @@
    27.4    Rule_Set.empty, NONE, []))]
    27.5  \<close>
    27.6  
    27.7 -(*ML_file "~~/test/Tools/isac/Specify/refine.sml" ... is called in Test_Isac.thy below,
    27.8 +(*ML_file "$ISABELLE_ISAC_TEST/Specify/refine.sml" ... is called in Test_Isac.thy below,
    27.9    so do NOT call it HERE; ?circularity*) 
   27.10  
   27.11  end

    28.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Apr 16 22:13:43 2021 +0200
    28.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Apr 16 22:29:23 2021 +0200
    28.3 @@ -3,10 +3,10 @@
    28.4     (c) copyright due to license terms.
    28.5  
    28.6     Isac's tests are organised parallel to sources: 
    28.7 -     "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
    28.8 +     $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
    28.9     plus
   28.10 -     ~~/test/Tools/isac/ADDTESTS
   28.11 -     ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
   28.12 +     $ISABELLE_ISAC_TEST/ADDTESTS
   28.13 +     $ISABELLE_ISAC_TEST/Minisubpbl: the Lucas-Interpreter's core functionality
   28.14  
   28.15  Note, that only the first error in a file is shown here.
   28.16  *)
   28.17 @@ -61,16 +61,16 @@
   28.18       and find out, which ML_file or *.thy causes an error (might be ONLY one).
   28.19       Also backup files (#* ) recognised by jEdit cause this trouble                    *)
   28.20  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
   28.21 -    "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
   28.22 -(**)"~~/test/Tools/isac/ADDTESTS/Ctxt"
   28.23 -(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"
   28.24 -(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt"
   28.25 -(**)"~~/test/Tools/isac/ADDTESTS/Test_Units"
   28.26 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
   28.27 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
   28.28 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
   28.29 -(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
   28.30 -(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
   28.31 +    "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
   28.32 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Ctxt"
   28.33 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/test-depend/Build_Test"
   28.34 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/All_Ctxt"
   28.35 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Test_Units"
   28.36 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T1_Basics"
   28.37 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T2_Rewriting"
   28.38 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T3_MathEngine"
   28.39 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/BuildC_Test"
   28.40 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory/Foo"
   28.41  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
   28.42     ADDTESTS/------------------------------------------- see end of tests *)
   28.43  (*/--- these work directly from Pure, but create problems here ..
   28.44 @@ -84,12 +84,12 @@
   28.45  (**)"~~/test/Pure/Isar/Test_Parsers"
   28.46  (**)"~~/test/Pure/Isar/Test_Parse_Term"
   28.47  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
   28.48 -  "~~/test/Tools/isac/Specify/refine"        (* setup for refine.sml   *)
   28.49 -  "~~/test/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)
   28.50 -  "~~/test/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)
   28.51 +  "$ISABELLE_ISAC_TEST/Specify/refine"        (* setup for refine.sml   *)
   28.52 +  "$ISABELLE_ISAC_TEST/ProgLang/calculate"    (* setup for evaluate.sml *)
   28.53 +  "$ISABELLE_ISAC_TEST/Knowledge/integrate"   (* setup for integrate.sml*)
   28.54  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
   28.55 -  "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
   28.56 -  "~~/src/Tools/isac/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)
   28.57 +  "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
   28.58 +  "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)
   28.59  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
   28.60  
   28.61  begin
   28.62 @@ -362,8 +362,8 @@
   28.63  
   28.64  section \<open>further tests additional to src/.. files\<close>
   28.65    ML_file "BridgeLibisabelle/use-cases.sml"
   28.66 -  ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
   28.67 -  ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
   28.68 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/mini-test.sml"
   28.69 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml"
   28.70  
   28.71    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   28.72    ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   28.73 @@ -511,7 +511,7 @@
   28.74    isac on Isabelle2012 is considered just a transitional stage
   28.75    within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
   28.76    For considerations on the transition see 
   28.77 -  ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
   28.78 +  $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
   28.79  \<close>
   28.80  subsubsection \<open>Run tests\<close>
   28.81  text \<open>

    29.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Fri Apr 16 22:13:43 2021 +0200
    29.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Apr 16 22:29:23 2021 +0200
    29.3 @@ -3,10 +3,10 @@
    29.4     (c) copyright due to license terms.
    29.5  
    29.6     Isac's tests are organised parallel to sources: 
    29.7 -     "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
    29.8 +     $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
    29.9     plus
   29.10 -     ~~/test/Tools/isac/ADDTESTS
   29.11 -     ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
   29.12 +     $ISABELLE_ISAC_TEST/ADDTESTS
   29.13 +     $ISABELLE_ISAC_TEST/Minisubpbl: the Lucas-Interpreter's core functionality
   29.14  
   29.15  Note, that only the first error in a file is shown here.
   29.16  *)
   29.17 @@ -61,16 +61,16 @@
   29.18       and find out, which ML_file or *.thy causes an error (might be ONLY one).
   29.19       Also backup files (#* ) recognised by jEdit cause this trouble                    *)
   29.20  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
   29.21 -    "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
   29.22 -(**)"~~/test/Tools/isac/ADDTESTS/Ctxt"
   29.23 -(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"
   29.24 -(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt"
   29.25 -(**)"~~/test/Tools/isac/ADDTESTS/Test_Units"
   29.26 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
   29.27 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
   29.28 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
   29.29 -(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
   29.30 -(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
   29.31 +    "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
   29.32 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Ctxt"
   29.33 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/test-depend/Build_Test"
   29.34 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/All_Ctxt"
   29.35 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Test_Units"
   29.36 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T1_Basics"
   29.37 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T2_Rewriting"
   29.38 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T3_MathEngine"
   29.39 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/BuildC_Test"
   29.40 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory/Foo"
   29.41  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
   29.42     ADDTESTS/------------------------------------------- see end of tests *)
   29.43  (*/--- these work directly from Pure, but create problems here ..
   29.44 @@ -83,12 +83,12 @@
   29.45  (**)"~~/test/Pure/Isar/Test_Parsers"
   29.46  (**)"~~/test/HOL/Tools/Sledgehammer/Try_Sledgehammer"
   29.47  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
   29.48 -  "~~/test/Tools/isac/Specify/refine"        (* setup for refine.sml   *)
   29.49 -  "~~/test/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)
   29.50 -  "~~/test/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)
   29.51 +  "$ISABELLE_ISAC_TEST/Specify/refine"        (* setup for refine.sml   *)
   29.52 +  "$ISABELLE_ISAC_TEST/ProgLang/calculate"    (* setup for evaluate.sml *)
   29.53 +  "$ISABELLE_ISAC_TEST/Knowledge/integrate"   (* setup for integrate.sml*)
   29.54  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
   29.55 -(*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)
   29.56 -(*"~~/src/Tools/isac/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)
   29.57 +(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)
   29.58 +(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)
   29.59  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
   29.60  
   29.61  begin
   29.62 @@ -330,8 +330,8 @@
   29.63  
   29.64  section \<open>further tests additional to src/.. files\<close>
   29.65    ML_file "BridgeLibisabelle/use-cases.sml"
   29.66 -  ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
   29.67 -  ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
   29.68 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/mini-test.sml"
   29.69 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml"
   29.70  
   29.71    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   29.72    ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   29.73 @@ -479,7 +479,7 @@
   29.74    isac on Isabelle2012 is considered just a transitional stage
   29.75    within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
   29.76    For considerations on the transition see 
   29.77 -  ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
   29.78 +  $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
   29.79  \<close>
   29.80  subsubsection \<open>Run tests\<close>
   29.81  text \<open>

    30.1 --- a/test/Tools/isac/Test_Theory.thy	Fri Apr 16 22:13:43 2021 +0200
    30.2 +++ b/test/Tools/isac/Test_Theory.thy	Fri Apr 16 22:29:23 2021 +0200
    30.3 @@ -1,9 +1,9 @@
    30.4  (* use this theory for tests before Build_Isac.thy has succeeded *)
    30.5 -theory Test_Theory imports "~~/src/Tools/isac/Specify/Specify"
    30.6 +theory Test_Theory imports "$ISABELLE_ISAC/Specify/Specify"
    30.7  begin                                                                            
    30.8 -ML_file "~~/src/Tools/isac/BaseDefinitions/libraryC.sml"
    30.9 +ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"
   30.10  (* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory
   30.11 -  requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *)
   30.12 +  requires session Isac, see $ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory *)
   30.13  
   30.14  section \<open>code for copy & paste ===============================================================\<close>
   30.15  ML \<open>