1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
;; (include-book "std/strings/istrprefixp" :dir :system)
;; (include-book "centaur/meta/def-formula-checks" :dir :system)
(include-book "centaur/meta/portcullis" :dir :system)
(include-book "centaur/bitops/portcullis" :dir :system)
(include-book "std/portcullis" :dir :system)
(defpkg "RP"
(union$ *acl2-exports*
;;*standard-acl2-imports*
*std-pkg-symbols*
*bitops-exports*
std::*std-exports*
'(acl2::and*
acl2::or*
b*
define
repeat
bash
bash-fn
bool-fix
repeat
rev
acl2::r
acl2::defsection
take-of-len-free
list-fix
suffixp
explode
enable*
e/d*
take-of-len-free
take-of-take-split
take-of-too-many
take-redefinition
tshell-start
true-listp-append
pos-listp
prefixp
prefixp-of-cons-left
prefixp-when-equal-lengths
proof-by-arith
append-of-cons
acl2::beta-reduce-lambda-expr
std::defret
std::defret-mutual
make-flag
str::natstr
str::iprefixp
str::istrprefixp
str::natchars
str::basic-natchars
acl2::symbol-list-listp
acl2::unprettify
acl2::vescmul
acl2::vescmul-verify
acl2::vescmul-parse
acl2::logapp
acl2::loghead
acl2::logbit
acl2::logbit$inline
acl2::logtail
acl2::Defines
acl2::patbind-ret
;;acl2::in
acl2::for
acl2::collect
;; acl2::sum
acl2::when
acl2::until
acl2::by
acl2::to
acl2::as
acl2::from
acl2::rp-rewriter
acl2::rp
acl2::sv
acl2::svl
acl2::defsvtv
acl2::vl
acl2::svtv-run
acl2::svl-run
acl2::svl-flatten-design
cmr::def-formula-checks
cmr::def-formula-checks-default-evl)
;;*common-lisp-symbols-from-main-lisp-package*
:test 'eq
))
|
