| changeset 1939 | ad5bb12605fb |
| parent 1730 | 1c7f793fc374 |
| child 1973 | 8c94c9a5be10 |
--- a/src/HOL/IMP/Transition.ML Thu Aug 22 12:27:01 1996 +0200 +++ b/src/HOL/IMP/Transition.ML Fri Aug 23 13:03:02 1996 +0200 @@ -129,7 +129,7 @@ goal Transition.thy "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \ -\ (c2,s2) -*-> (c3,s3) --> (c1;c2,s1) -*-> (c3,s3)"; +\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; be converse_rtrancl_induct2 1; by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);