src/Tools/isac/Build_Isac.thy
changeset 55459 339639ffde0e
parent 55454 04438781cef7
child 55484 7df94616c1bd
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Jun 22 14:58:51 2014 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Jun 22 15:17:07 2014 +0200
     1.3 @@ -87,10 +87,6 @@
     1.4  *}
     1.5  subsection {* (0) Survey on remaining Unsynchronized.ref *}
     1.6  text {*
     1.7 -  REMOVE WITHOUT REPLACEMENT (requires some efforts)
     1.8 -    calcelems.sml:val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);
     1.9 -    calcelems.sml:val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);
    1.10 -    calcelems.sml:val isabthys = Unsynchronized.ref ([] : theory list);
    1.11    REPLACE BY KEStore... (has been overlooked)
    1.12      calcelems.sml:val rew_ord' = Unsynchronized.ref ...
    1.13    KEEP FOR TRACING