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

« back to all changes in this revision

Viewing changes to books/rtl/rel5/arithmetic/expo.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:
64
64
 
65
65
 
66
66
(theory-invariant
67
 
 (not (and (or (member-equal '(:rewrite expo-minus)
68
 
                             theory)
69
 
               (member-equal '(:rewrite expo-minus-eric)
70
 
                             theory))
71
 
           (member-equal '(:definition expo)
72
 
                         theory)))
 
67
 (not (and (or (active-runep '(:rewrite expo-minus))
 
68
               (active-runep '(:rewrite expo-minus-eric)))
 
69
           (active-runep '(:definition expo))))
73
70
 :key expo-minus-invariant)
74
71
 
75
72
;Eric doesn't like the presence of ABS here...