equal
deleted
inserted
replaced
143 "xx" |
143 "xx" |
144 ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) |
144 ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) |
145 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*) |
145 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*) |
146 \<close> ML \<open> |
146 \<close> ML \<open> |
147 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*) |
147 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*) |
148 Rewrite.trace_on := false; |
|
149 \<close> |
148 \<close> |
150 ML \<open> |
149 ML \<open> |
151 \<close> ML \<open> |
|
152 \<close> ML \<open> |
|
153 \<close> ML \<open> |
|
154 \<close> ML \<open> |
|
155 \<close> ML \<open> |
|
156 \<close> ML \<open> |
|
157 \<close> ML \<open> |
150 \<close> ML \<open> |
158 \<close> ML \<open> |
151 \<close> ML \<open> |
159 \<close> ML \<open> |
152 \<close> ML \<open> |
160 \<close> ML \<open> |
153 \<close> ML \<open> |
161 \<close> |
154 \<close> |
327 |
320 |
328 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
321 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
329 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
322 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
330 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
323 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
331 ML \<open> |
324 ML \<open> |
332 \<close> ML \<open> |
|
333 \<close> ML \<open> |
|
334 \<close> ML \<open> |
|
335 \<close> ML \<open> |
|
336 \<close> ML \<open> |
|
337 \<close> ML \<open> |
|
338 \<close> ML \<open> |
325 \<close> ML \<open> |
339 \<close> ML \<open> |
326 \<close> ML \<open> |
340 \<close> ML \<open> |
327 \<close> ML \<open> |
341 \<close> ML \<open> |
328 \<close> ML \<open> |
342 \<close> |
329 \<close> |