1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Fri Apr 16 22:13:43 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Apr 16 22:29:23 2021 +0200
     1.3 @@ -3,10 +3,10 @@
     1.4     (c) copyright due to license terms.
     1.5  
     1.6     Isac's tests are organised parallel to sources: 
     1.7 -     "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
     1.8 +     $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
     1.9     plus
    1.10 -     ~~/test/Tools/isac/ADDTESTS
    1.11 -     ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
    1.12 +     $ISABELLE_ISAC_TEST/ADDTESTS
    1.13 +     $ISABELLE_ISAC_TEST/Minisubpbl: the Lucas-Interpreter's core functionality
    1.14  
    1.15  Note, that only the first error in a file is shown here.
    1.16  *)
    1.17 @@ -61,16 +61,16 @@
    1.18       and find out, which ML_file or *.thy causes an error (might be ONLY one).
    1.19       Also backup files (#* ) recognised by jEdit cause this trouble                    *)
    1.20  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    1.21 -    "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
    1.22 -(**)"~~/test/Tools/isac/ADDTESTS/Ctxt"
    1.23 -(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"
    1.24 -(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt"
    1.25 -(**)"~~/test/Tools/isac/ADDTESTS/Test_Units"
    1.26 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
    1.27 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
    1.28 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
    1.29 -(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
    1.30 -(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
    1.31 +    "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
    1.32 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Ctxt"
    1.33 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/test-depend/Build_Test"
    1.34 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/All_Ctxt"
    1.35 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Test_Units"
    1.36 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T1_Basics"
    1.37 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T2_Rewriting"
    1.38 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T3_MathEngine"
    1.39 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/BuildC_Test"
    1.40 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory/Foo"
    1.41  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
    1.42     ADDTESTS/------------------------------------------- see end of tests *)
    1.43  (*/--- these work directly from Pure, but create problems here ..
    1.44 @@ -83,12 +83,12 @@
    1.45  (**)"~~/test/Pure/Isar/Test_Parsers"
    1.46  (**)"~~/test/HOL/Tools/Sledgehammer/Try_Sledgehammer"
    1.47  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    1.48 -  "~~/test/Tools/isac/Specify/refine"        (* setup for refine.sml   *)
    1.49 -  "~~/test/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)
    1.50 -  "~~/test/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)
    1.51 +  "$ISABELLE_ISAC_TEST/Specify/refine"        (* setup for refine.sml   *)
    1.52 +  "$ISABELLE_ISAC_TEST/ProgLang/calculate"    (* setup for evaluate.sml *)
    1.53 +  "$ISABELLE_ISAC_TEST/Knowledge/integrate"   (* setup for integrate.sml*)
    1.54  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
    1.55 -(*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)
    1.56 -(*"~~/src/Tools/isac/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)
    1.57 +(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)
    1.58 +(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)
    1.59  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
    1.60  
    1.61  begin
    1.62 @@ -330,8 +330,8 @@
    1.63  
    1.64  section \<open>further tests additional to src/.. files\<close>
    1.65    ML_file "BridgeLibisabelle/use-cases.sml"
    1.66 -  ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
    1.67 -  ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
    1.68 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/mini-test.sml"
    1.69 +  ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml"
    1.70  
    1.71    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.72    ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.73 @@ -479,7 +479,7 @@
    1.74    isac on Isabelle2012 is considered just a transitional stage
    1.75    within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
    1.76    For considerations on the transition see 
    1.77 -  ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
    1.78 +  $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
    1.79  \<close>
    1.80  subsubsection \<open>Run tests\<close>
    1.81  text \<open>