new directory for Integers
authorpaulson
Tue, 22 Sep 1998 15:24:01 +0200
changeset 5532 69fdc4f883a0
parent 5531 75356cabe3bb
child 5533 bce36a019b03
new directory for Integers
src/ZF/Integ/Integ.ML
--- 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];