src/Tools/isac/ProgLang/Script.thy
branchisac-update-Isa09-2
changeset 38007 d679c1f837a7
parent 38006 16d56796f5a0
child 38051 efdeff9df986
equal deleted inserted replaced
38006:16d56796f5a0 38007:d679c1f837a7
   183   (distinct (remove op = "" 
   183   (distinct (remove op = "" 
   184              (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));
   184              (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));
   185 
   185 
   186 val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
   186 val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
   187 
   187 
   188 val tacpbl = ref
   188 val tacpbl = Unsynchronized.ref
   189   (distinct (remove op = "" (!tacs (*@ !subpbls*))));
   189   (distinct (remove op = "" (!tacs (*@ !subpbls*))));
   190 (*--^^^----- SHIFT? or delete ?*)
   190 (*--^^^----- SHIFT? or delete ?*)
   191 
   191 
   192 *}
   192 *}
   193 
   193