no \<^isac_test> guard for test material: thus the Prover IDE does not have to switch the option "isac_test";
authorwenzelm
Mon, 19 Apr 2021 19:55:31 +0200
changeset 60236de0ccac9f862
parent 60235 0d11e9bab8de
child 60237 e534316f9e07
no \<^isac_test> guard for test material: thus the Prover IDE does not have to switch the option "isac_test";
test/Tools/isac/Test_Isac.thy
test/Tools/isac/Test_Isac_Short.thy
test/Tools/isac/Test_Some.thy
test/Tools/isac/Test_Some_meld.thy
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Apr 19 18:05:01 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Apr 19 19:55:31 2021 +0200
     1.3 @@ -96,9 +96,6 @@
     1.4  
     1.5  ML \<open>open ML_System\<close>
     1.6  ML \<open>
     1.7 -\<^isac_test>\<open>
     1.8 -                      (* these vvv test, if funs are intermediately opened in structure 
     1.9 -                         in case of errors here consider ~~/xtest-to-coding.sh      *)
    1.10    open Kernel;
    1.11    open Math_Engine;
    1.12    open Test_Code;              CalcTreeTEST;
    1.13 @@ -143,7 +140,6 @@
    1.14    open Rewrite_Ord
    1.15    open UnparseC
    1.16  \<close>
    1.17 -\<close>
    1.18  ML_file "BaseDefinitions/libraryC.sml"
    1.19  
    1.20  section \<open>code for copy & paste ===============================================================\<close>
     2.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 19 18:05:01 2021 +0200
     2.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 19 19:55:31 2021 +0200
     2.3 @@ -95,9 +95,6 @@
     2.4  
     2.5  ML \<open>open ML_System\<close>
     2.6  ML \<open>
     2.7 -\<^isac_test>\<open>
     2.8 -                      (* these vvv test, if funs are intermediately opened in structure 
     2.9 -                         in case of errors here consider ~~/xtest-to-coding.sh      *)
    2.10    open Kernel;
    2.11    open Math_Engine;
    2.12    open Test_Code;              CalcTreeTEST;
    2.13 @@ -142,7 +139,6 @@
    2.14    open Rewrite_Ord
    2.15    open UnparseC
    2.16  \<close>
    2.17 -\<close>
    2.18  
    2.19  ML \<open>
    2.20  "~~~~~ fun xxx , args:"; val () = ();
     3.1 --- a/test/Tools/isac/Test_Some.thy	Mon Apr 19 18:05:01 2021 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Mon Apr 19 19:55:31 2021 +0200
     3.3 @@ -4,9 +4,6 @@
     3.4  
     3.5  ML \<open>open ML_System\<close>
     3.6  ML \<open>
     3.7 -\<^isac_test>\<open>
     3.8 -                      (* these vvv test, if funs are intermediately opened in structure 
     3.9 -                         in case of errors here consider ~~/xtest-to-coding.sh      *)
    3.10    open Kernel;
    3.11    open Math_Engine;
    3.12    open Test_Code;              CalcTreeTEST;
    3.13 @@ -51,7 +48,6 @@
    3.14    open Rewrite_Ord
    3.15    open UnparseC
    3.16  \<close>
    3.17 -\<close>
    3.18  ML_file "BridgeJEdit/parseC.sml"
    3.19  
    3.20  section \<open>code for copy & paste ===============================================================\<close>
     4.1 --- a/test/Tools/isac/Test_Some_meld.thy	Mon Apr 19 18:05:01 2021 +0200
     4.2 +++ b/test/Tools/isac/Test_Some_meld.thy	Mon Apr 19 19:55:31 2021 +0200
     4.3 @@ -1,9 +1,6 @@
     4.4  theory Test_Some_meld imports Isac.Build_Thydata
     4.5  begin 
     4.6  ML \<open>
     4.7 -\<^isac_test>\<open>
     4.8 -                      (* these vvv test, if funs are intermediately opened in structure 
     4.9 -                         in case of errors here consider ~~/xtest-to-coding.sh      *)
    4.10    open Kernel;
    4.11    open Math_Engine;
    4.12    open LItool;                  arguments_from_model;
    4.13 @@ -27,7 +24,6 @@
    4.14    open TermC;                  atomt;
    4.15    open Rule;                   ThmC.string_of_thm;
    4.16  \<close>
    4.17 -\<close>
    4.18  ML_file "BaseDefinitions/libraryC.sml"
    4.19  
    4.20  section \<open>code for copy & paste ===============================================================\<close>