| commit | c51b7fd65b8c7476180c965d48390431b2d558e6 | [log] [tgz] |
|---|---|---|
| author | Stefan Krah <skrah@bytereef.org> | Wed Apr 18 19:27:32 2012 +0200 |
| committer | Stefan Krah <skrah@bytereef.org> | Wed Apr 18 19:27:32 2012 +0200 |
| tree | 5fb4e132eddf655bdda222bfda9a2f96784fdcd4 | |
| parent | 5d0d2e2b04631e5ad9c7dad60e6be75c02f8e050 [diff] |
1) Simplify comment -- one has to read the complete proof (available in ACL2) in order to understand the algorithm anyway. 2) v->exp == -v->digits may be assumed. 3) Fix comment (v always shares data with a).