equal
deleted
inserted
replaced
294 INV {\<exists>ps. Path tl p ps X} |
294 INV {\<exists>ps. Path tl p ps X} |
295 DO p := p^.tl OD |
295 DO p := p^.tl OD |
296 {p = X}" |
296 {p = X}" |
297 apply vcg_simp |
297 apply vcg_simp |
298 apply blast |
298 apply blast |
299 apply clarsimp |
|
300 apply(erule disjE) |
|
301 apply clarsimp |
|
302 apply fastsimp |
299 apply fastsimp |
303 apply clarsimp |
300 apply clarsimp |
304 done |
301 done |
305 |
302 |
306 text{*Now it dawns on us that we do not need the list witness at all --- it |
303 text{*Now it dawns on us that we do not need the list witness at all --- it |