1.1 --- a/test/ROOT Tue Feb 07 17:25:09 2023 +0100
1.2 +++ b/test/ROOT Tue Feb 07 17:43:16 2023 +0100
1.3 @@ -26,7 +26,6 @@
1.4 "ADDTESTS/file-depend"
1.5 "ADDTESTS/file-depend/1language"
1.6 "ADDTESTS/file-depend/3knowledge"
1.7 - "ADDTESTS/session-get_theory"
1.8 "ADDTESTS/test-depend"
1.9 "ADDTESTS/test-depend/testdir1"
1.10 "ADDTESTS/test-depend/testdirm"
2.1 --- a/test/Tools/isac/Test_Isac.thy Tue Feb 07 17:25:09 2023 +0100
2.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Feb 07 17:43:16 2023 +0100
2.3 @@ -60,7 +60,6 @@
2.4 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
2.5 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
2.6 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
2.7 -(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
2.8 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
2.9 ADDTESTS/------------------------------------------- see end of tests *)
2.10 (*/~~~ these work directly from Pure, but create problems here ..
3.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Feb 07 17:25:09 2023 +0100
3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Feb 07 17:43:16 2023 +0100
3.3 @@ -60,7 +60,6 @@
3.4 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
3.5 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
3.6 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
3.7 -(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
3.8 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
3.9 ADDTESTS/------------------------------------------- see end of tests *)
3.10 (*/~~~ these work directly from Pure, but create problems here ..
4.1 --- a/test/Tools/isac/Test_Theory.thy Tue Feb 07 17:25:09 2023 +0100
4.2 +++ b/test/Tools/isac/Test_Theory.thy Tue Feb 07 17:43:16 2023 +0100
4.3 @@ -2,8 +2,6 @@
4.4 theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"
4.5 begin
4.6 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"
4.7 -(* ATTENTION: tests with Test_Code.init_calc, CalcTree @{context} do NOT work here, because Thy_Info.get_theory
4.8 - requires session Isac, see $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory *)
4.9
4.10 section \<open>code for copy & paste ===============================================================\<close>
4.11 ML \<open>