Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generalized my_lemma1: (c3,s3) |--> cs3
authornipkow
Fri, 23 Aug 1996 13:03:02 +0200
changeset 1939 ad5bb12605fb
parent 1938 4e29ea45520d
child 1940 9bd1c8826f5c
Generalized my_lemma1: (c3,s3) |--> cs3
src/HOL/IMP/Transition.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle