eliminate use of Thy_Info 24: finished
authorwneuper <Walther.Neuper@jku.at>
Tue, 07 Feb 2023 17:43:16 +0100
changeset 606773e9cb1527f02
parent 60676 8c37f1009457
child 60678 4b5be1a53e17
eliminate use of Thy_Info 24: finished
test/ROOT
test/Tools/isac/Test_Isac.thy
test/Tools/isac/Test_Isac_Short.thy
test/Tools/isac/Test_Theory.thy
     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>