changeset 804 | 02430d273ebf |
parent 782 | 200a16083201 |
child 904 | 5240dcd12adb |
--- a/src/ZF/ex/Integ.ML Fri Dec 16 18:07:12 1994 +0100 +++ b/src/ZF/ex/Integ.ML Mon Dec 19 13:01:30 1994 +0100 @@ -143,7 +143,7 @@ goalw Integ.thy [znegative_def, znat_def] "~ znegative($# n)"; by (asm_full_simp_tac (intrel_ss setloop K(safe_tac intrel_cs)) 1); -be rev_mp 1; +by (etac rev_mp 1); by (asm_simp_tac (arith_ss addsimps [add_le_self2 RS le_imp_not_lt]) 1); qed "not_znegative_znat";