← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/nonstd/nsa/equivalence-derivatives.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/nonstd/nsa/equivalence-derivatives.lisp
691
691
                 )
692
692
           :in-theory (disable i-close-transitive
693
693
                               i-close-limited
694
 
                               standard-derivative-rdfn-classical)
 
694
                               standard-derivative-rdfn-classical
 
695
; Added by Matt K., 12/5/2014: The proof seemed to take very long (forever?)
 
696
; today (I don't know why), but it succeeds quickly with the following
 
697
; additional disables.  Actually only one of these needs to be disabled, but
 
698
; compared to disabling both, the proof takes about 10x longer if only the
 
699
; second is enabled and about 27x as long if only the first is enabled.
 
700
                               DIFFERENTIAL-RDFN2-LIMITED
 
701
                               CLOSE-IF-<-ABS
 
702
                               )
695
703
           )
696
704
          )
697
705
  )