diff -r d0ad1d3b8671 -r 1d9fee958a46 test/Tools/isac/Test_Isac_Short.thy
--- a/test/Tools/isac/Test_Isac_Short.thy	Sun Apr 18 16:30:11 2021 +0200
+++ b/test/Tools/isac/Test_Isac_Short.thy	Sun Apr 18 18:30:31 2021 +0200
@@ -5,8 +5,8 @@
    Isac's tests are organised parallel to sources: 
      $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
    plus
-     $ISABELLE_ISAC_TEST/ADDTESTS
-     $ISABELLE_ISAC_TEST/Minisubpbl: the Lucas-Interpreter's core functionality
+     $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS
+     $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
 
 Note, that only the first error in a file is shown here.
 *)
@@ -61,31 +61,31 @@
      and find out, which ML_file or *.thy causes an error (might be ONLY one).
      Also backup files (#* ) recognised by jEdit cause this trouble                    *)
 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
-    "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Ctxt"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/test-depend/Build_Test"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/All_Ctxt"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Test_Units"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T1_Basics"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T2_Rewriting"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T3_MathEngine"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/BuildC_Test"
-(**)"$ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory/Foo"
+    "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
+(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
    ADDTESTS/------------------------------------------- see end of tests *)
 (*/--- these work directly from Pure, but create problems here ..
-  "~~/test/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)
-  "~~/test/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)
-  "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)
-  "~~/test/Pure/Isar/Theory_Commands"            (* Duplicate outer syntax command "ISAC"   *)
-  "~~/test/Pure/Isar/Downto_Synchronized"        (* re-defines / breaks structures      !!! *)
+  "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)
+  "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)
+  "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)
+  "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands"            (* Duplicate outer syntax command "ISAC"   *)
+  "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized"        (* re-defines / breaks structures      !!! *)
   \--- .. these work independently, but create problems here *)
-(**)"~~/test/Pure/Isar/Test_Parsers"
-(**)"~~/test/HOL/Tools/Sledgehammer/Try_Sledgehammer"
+(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
+(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
-  "$ISABELLE_ISAC_TEST/Specify/refine"        (* setup for refine.sml   *)
-  "$ISABELLE_ISAC_TEST/ProgLang/calculate"    (* setup for evaluate.sml *)
-  "$ISABELLE_ISAC_TEST/Knowledge/integrate"   (* setup for integrate.sml*)
+  "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine"        (* setup for refine.sml   *)
+  "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)
+  "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)
 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)
 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)
@@ -175,10 +175,10 @@
   ---------------------- check test file by testfile -------------------------------------------*)
 section \<open>trials with Isabelle's functions\<close>
   ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
-  ML_file "~~/test/Pure/General/alist.ML"
-  ML_file "~~/test/Pure/General/basics.ML"
-  ML_file "~~/test/Pure/General/scan.ML"
-  ML_file "~~/test/Pure/PIDE/xml.ML"
+  ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
+  ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
+  ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
+  ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
   ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
 
 section \<open>test ML Code of isac\<close>
@@ -330,8 +330,8 @@
 
 section \<open>further tests additional to src/.. files\<close>
   ML_file "BridgeLibisabelle/use-cases.sml"
-  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/mini-test.sml"
-  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml"
+  ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
+  ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
 
   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>