← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel5/lib/basic.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel5/lib/basic.lisp
178
178
  :rule-classes ())
179
179
 
180
180
(defthm mod-0
181
 
  (implies (acl2-numberp x)
182
 
           (equal (mod x 0) x)))
 
181
    (and (equal (mod 0 y)
 
182
                0)
 
183
         (equal (mod x 0)
 
184
                (fix x))))
183
185
 
184
186
(defthm rationalp-mod
185
187
  (implies (case-split (rationalp x))