author | paulson |
Tue, 22 Sep 1998 15:24:01 +0200 | |
changeset 5532 | 69fdc4f883a0 |
parent 5531 | 75356cabe3bb |
child 5533 | bce36a019b03 |
--- a/src/ZF/Integ/Integ.ML Tue Sep 22 15:23:39 1998 +0200 +++ b/src/ZF/Integ/Integ.ML Tue Sep 22 15:24:01 1998 +0200 @@ -144,8 +144,8 @@ by Safe_tac; by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1); by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1); -by (fast_tac (claset() addss - (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1); +by (force_tac (claset(), + simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1); qed "not_znegative_znat"; Addsimps [not_znegative_znat];