1.1 --- a/src/Tools/isac/Build_Isac.thy	Wed Aug 03 17:18:47 2022 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Aug 03 18:06:02 2022 +0200
     1.3 @@ -200,12 +200,7 @@
     1.4  \<close>
     1.5  subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
     1.6  text \<open>
     1.7 -  REPLACE BY Know_Store... (has been overlooked)
     1.8 -    calcelems.sml:val rew_ord' = Unsynchronized.ref ...
     1.9 -  KEEP FOR DEMOS
    1.10 -    Knowledge/GCD_Poly_ML.thy:  val trace_div = Unsynchronized.ref true;
    1.11 -    Knowledge/GCD_Poly_ML.thy:  val trace_div_invariant = Unsynchronized.ref false;
    1.12 -    Knowledge/GCD_Poly_ML.thy:  val trace_Euclid = Unsynchronized.ref true;
    1.13 +  DONE
    1.14  \<close>
    1.15  subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
    1.16  subsection \<open>(2) Make Isac’s programming language usable\<close>