equal
deleted
inserted
replaced
403 by (rtac hoare_derivs.Local 1); |
403 by (rtac hoare_derivs.Local 1); |
404 by (etac conseq2 1); |
404 by (etac conseq2 1); |
405 by (etac spec 1); |
405 by (etac spec 1); |
406 qed "weak_Local"; |
406 qed "weak_Local"; |
407 |
407 |
|
408 (* |
|
409 Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}"; |
|
410 by (induct_tac "c" 1); |
|
411 auto(); |
|
412 br conseq1 1; |
|
413 br hoare_derivs.Skip 1; |
|
414 force 1; |
|
415 br conseq1 1; |
|
416 br hoare_derivs.Ass 1; |
|
417 force 1; |
|
418 by (defer_tac 1); |
|
419 ### |
|
420 br hoare_derivs.Comp 1; |
|
421 bd spec 2; |
|
422 bd spec 2; |
|
423 ba 2; |
|
424 be conseq1 2; |
|
425 by (Clarsimp_tac 2); |
|
426 force 1; |
|
427 *) |