← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/rtl/rel4/arithmetic/fp2.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel4/arithmetic/fp2.lisp
105
105
 
106
106
|#
107
107
 
108
 
;I want to use some theoremes in arithmetic-2, but the theorems I want to prove have the same names as those,
 
108
;I want to use some theoremes in arithmetic 2, but the theorems I want to prove have the same names as those,
109
109
;so I export them from the encapsulate with -alt appended to the names.
110
110
 
111
111
 
112
112
(local 
113
113
 (encapsulate 
114
114
  ()
115
 
             
116
 
  (local (include-book "arithmetic-2/meta/non-linear" :dir :system))
 
115
  ;; [Jared] changed this to use arithmetic-3 instead of 2.
 
116
  (local (include-book "arithmetic-3/bind-free/top" :dir :system))
117
117
 
118
118
;BOZO generalize the (rationalp x) hyp (is it enough that, say, y be rational?)
119
 
  (defthm *-weakly-monotonic-alt
 
119
 (defthm *-weakly-monotonic-alt
120
120
    (implies (and (<= y y+)
121
121
                  (<= 0 x) ;reordered to put this first!
122
122
                  (rationalp x) ; This does not hold if x, y, and z are complex!