changeset 3439 | 54785105178c |
parent 3023 | 01364e2f30ad |
child 4089 | 96fba19bcbe2 |
--- a/src/HOL/IMP/Transition.ML Mon Jun 16 14:25:33 1997 +0200 +++ b/src/HOL/IMP/Transition.ML Tue Jun 17 09:01:56 1997 +0200 @@ -128,7 +128,7 @@ goal Transition.thy "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \ \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; -by (etac converse_rtrancl_induct2 1); +by (etac inverse_rtrancl_induct2 1); by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); qed_spec_mp "my_lemma1";