src/HOL/IMP/Transition.ML
changeset 1939 ad5bb12605fb
parent 1730 1c7f793fc374
child 1973 8c94c9a5be10
equal deleted inserted replaced
1938:4e29ea45520d 1939:ad5bb12605fb
   127 
   127 
   128 section "A Proof Without -n->";
   128 section "A Proof Without -n->";
   129 
   129 
   130 goal Transition.thy
   130 goal Transition.thy
   131  "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
   131  "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
   132 \ (c2,s2) -*-> (c3,s3) --> (c1;c2,s1) -*-> (c3,s3)";
   132 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
   133 be converse_rtrancl_induct2 1;
   133 be converse_rtrancl_induct2 1;
   134 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
   134 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
   135 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
   135 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
   136 qed_spec_mp "my_lemma1";
   136 qed_spec_mp "my_lemma1";
   137 
   137