← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/esim/stv/stv-compile.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/centaur/esim/stv/stv-compile.lisp
47
47
(local (include-book "../esim-sexpr-support-thms"))
48
48
(local (include-book "centaur/vl/util/arithmetic" :dir :system))
49
49
 
50
 
(make-event
51
 
 
52
 
; Disabling waterfall parallelism because this book allegedly uses memoization
53
 
; while performing its proofs.
54
 
 
55
 
 (if (and (hons-enabledp state)
56
 
          (f-get-global 'parallel-execution-enabled state))
57
 
     (er-progn (set-waterfall-parallelism nil)
58
 
               (value '(value-triple nil)))
59
 
   (value '(value-triple nil))))
60
 
 
61
50
(local (defthm atom-listp-of-pat-flatten1
62
51
         (atom-listp (pat-flatten1 x))
63
52
         :hints(("Goal" :in-theory (e/d (pat-flatten1)