src/HOL/IMP/Transition.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4477 b3e5857d8d99
     1.1 --- a/src/HOL/IMP/Transition.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/IMP/Transition.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -87,7 +87,7 @@
     1.4  
     1.5  (* ASSIGN *)
     1.6  by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]
     1.7 -                      addss simpset()) 1);
     1.8 +                       addss simpset()) 1);
     1.9  
    1.10  (* SEMI *)
    1.11  by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
    1.12 @@ -98,8 +98,7 @@
    1.13  by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1);
    1.14  
    1.15  (* WHILE, induction on the length of the computation *)
    1.16 -by (rotate_tac 1 1);
    1.17 -by (etac rev_mp 1);
    1.18 +by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
    1.19  by (res_inst_tac [("x","s")] spec 1);
    1.20  by (res_inst_tac [("n","n")] less_induct 1);
    1.21  by (strip_tac 1);