# HG changeset patch
# User nipkow
# Date 840798182 -7200
# Node ID ad5bb12605fbdf66f4c7f507ac600d61df8b1ea3
# Parent  4e29ea45520de2b88477fa6f8f2b0d89929628ef
Generalized my_lemma1: (c3,s3) |--> cs3

diff -r 4e29ea45520d -r ad5bb12605fb src/HOL/IMP/Transition.ML
--- 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);