| changeset 5168 | adafef6eb295 |
| parent 5137 | 60205b0de9b9 |
| child 5268 | 59ef39008514 |
--- a/src/ZF/ex/Integ.ML Tue Jul 21 08:54:09 1998 +0200 +++ b/src/ZF/ex/Integ.ML Tue Jul 21 12:12:52 1998 +0200 @@ -140,7 +140,7 @@ Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))"; by (asm_simp_tac (simpset() addsimps [zminus]) 1); -by(blast_tac (claset() addIs [nat_0_le]) 1); +by (blast_tac (claset() addIs [nat_0_le]) 1); qed "znegative_zminus_znat";