src/ZF/arith_data.ML
changeset 58838 59203adfc33f
parent 54388 8b165615ffe3
child 59498 50b60f501b05
     1.1 --- a/src/ZF/arith_data.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/ZF/arith_data.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5  (*Apply the given rewrite (if present) just once*)
     1.6  fun gen_trans_tac th2 NONE      = all_tac
     1.7 -  | gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2));
     1.8 +  | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve_tac [th RS th2]);
     1.9  
    1.10  (*Use <-> or = depending on the type of t*)
    1.11  fun mk_eq_iff(t,u) =