| changeset 9548 | 15bee2731e43 |
| parent 9000 | c20d58286a51 |
| child 9570 | e16e168984e1 |
--- a/src/ZF/ex/BinEx.ML Mon Aug 07 10:29:04 2000 +0200 +++ b/src/ZF/ex/BinEx.ML Mon Aug 07 10:29:54 2000 +0200 @@ -26,12 +26,12 @@ by (Simp_tac 1); (*300 msec*) result(); -Goal "$~ #65745 = #-65745"; +Goal "$- #65745 = #-65745"; by (Simp_tac 1); (*80 msec*) result(); (* negation of ~54321 *) -Goal "$~ #-54321 = #54321"; +Goal "$- #-54321 = #54321"; by (Simp_tac 1); (*90 msec*) result();