acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / tools / rulesets.cert

This file is indexed.

/usr/share/acl2-6.3/books/tools/rulesets.cert is in acl2-books-certs 6.3-5.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "XDOC" (SET-DIFFERENCE-EQ (UNION-EQ (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (B* QUIT EXIT VALUE DEFXDOC DEFXDOC-RAW MACRO-ARGS XDOC-EXTEND DEFSECTION DEFSECTION-PROGN CUTIL LNFIX SET-DEFAULT-PARENTS GETPROP FORMALS JUSTIFICATION DEF-BODIES CURRENT-ACL2-WORLD DEF-BODY ACCESS THEOREM UNTRANSLATED-THEOREM GUARD XDOC XDOC! UNQUOTE UNDOCUMENTED ASSERT! TOP EXPLODE IMPLODE))) (QUOTE NIL)) NIL ((:SYSTEM . "xdoc/portcullis.lisp") (:SYSTEM . "xdoc/top.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (DEFXDOC RULESETS :PARENTS (THEORIES DEFTHEORY) :SHORT "Table-based alternative to ACL2's named theories." :LONG "<p>Rulesets are like @(see theories), but can be extended with
additional rules after first being defined.  That is, you can build up a
ruleset incrementally, across many books, instead of having to define it all at
once and having it be forever fixed.</p>

<p>Basic usage of rulesets is just like theories.  You can:</p>

<ul>
<li>Introduce rulesets with @(see def-ruleset)</li>
<li>Extend existing rulesets with @(see add-to-ruleset).</li>
<li>Enable/disable rulesets with @(see enable*), @(see disable*), and @(see
e/d*)</li>
</ul>

<p>When we define a new package @('FOO'), we often set up @('FOO::enable') as
an alias for @('enable*'), to make using rulesets more convenient.</p>

<p>Advanced users can do some nifty things with rulesets, e.g., you can have a
superior ruleset that contains other rulesets, and it will grow as you add
rules to the contained rulesets.</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . RULESETS) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS THEORIES DEFTHEORY) (:SHORT . "Table-based alternative to ACL2's named theories.") (:LONG . "<p>Rulesets are like @(see theories), but can be extended with
additional rules after first being defined.  That is, you can build up a
ruleset incrementally, across many books, instead of having to define it all at
once and having it be forever fixed.</p>

<p>Basic usage of rulesets is just like theories.  You can:</p>

<ul>
<li>Introduce rulesets with @(see def-ruleset)</li>
<li>Extend existing rulesets with @(see add-to-ruleset).</li>
<li>Enable/disable rulesets with @(see enable*), @(see disable*), and @(see
e/d*)</li>
</ul>

<p>When we define a new package @('FOO'), we often set up @('FOO::enable') as
an alias for @('enable*'), to make using rulesets more convenient.</p>

<p>Advanced users can do some nifty things with rulesets, e.g., you can have a
superior ruleset that contains other rulesets, and it will grow as you add
rules to the contained rulesets.</p>") (:FROM . "[books]/tools/rulesets.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC RULESETS)))))) (17 RECORD-EXPANSION (DEFSECTION DEF-RULESET :PARENTS (RULESETS) :SHORT "@(call def-ruleset) creates a new ruleset." :LONG "<p>Examples:</p>
@({
 (def-ruleset my-rules
   '(append reverse))

 (def-ruleset other-rules
   '(member-equal my-rules revappend))
})

<p>The first example creates a new ruleset, @('my-rules'), with only the
definitions of @('append') and @('reverse').</p>

<p>The section example creates a new ruleset, @('other-rules'), with the
definitions of @('member-equal') and @('revappend'), and also a link to
@('my-rules').  When rules are added to @('my-rules'), @('other-rules')
also grows.</p>" (DEFMACRO DEF-RULESET (NAME FORM) (DECLARE (XARGS :GUARD (SYMBOLP NAME))) (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE WORLD) (CONS (CONS (QUOTE W) (CONS (QUOTE STATE) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE NAME) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE ER-PROGN) (CONS (CONS (QUOTE CHECK-NOT-RULESET) (CONS (QUOTE NAME) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL))))) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE RULES) (CONS (RULESET-FORM-PREPROCESS FORM) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DEF-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE DEF-RULESET)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO DEF-RULESET (NAME FORM) (DECLARE (XARGS :GUARD (SYMBOLP NAME))) (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE WORLD) (CONS (CONS (QUOTE W) (CONS (QUOTE STATE) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE NAME) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE ER-PROGN) (CONS (CONS (QUOTE CHECK-NOT-RULESET) (CONS (QUOTE NAME) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL))))) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE RULES) (CONS (RULESET-FORM-PREPROCESS FORM) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE DEF-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE DEF-RULESET)) (XDOC::PARENTS (QUOTE (RULESETS))) (XDOC::SHORT (QUOTE "@(call def-ruleset) creates a new ruleset.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE DEF-RULESET))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Examples:</p>
@({
 (def-ruleset my-rules
   '(append reverse))

 (def-ruleset other-rules
   '(member-equal my-rules revappend))
})

<p>The first example creates a new ruleset, @('my-rules'), with only the
definitions of @('append') and @('reverse').</p>

<p>The section example creates a new ruleset, @('other-rules'), with the
definitions of @('member-equal') and @('revappend'), and also a link to
@('my-rules').  When rules are added to @('my-rules'), @('other-rules')
also grows.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . DEF-RULESET) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RULESETS) (:SHORT . "@(call def-ruleset) creates a new ruleset.") (:LONG . "<p>Examples:</p>
@({
 (def-ruleset my-rules
   '(append reverse))

 (def-ruleset other-rules
   '(member-equal my-rules revappend))
})

<p>The first example creates a new ruleset, @('my-rules'), with only the
definitions of @('append') and @('reverse').</p>

<p>The section example creates a new ruleset, @('other-rules'), with the
definitions of @('member-equal') and @('revappend'), and also a link to
@('my-rules').  When rules are added to @('my-rules'), @('other-rules')
also grows.</p>

") (:FROM . "[books]/tools/rulesets.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC DEF-RULESET)))))) (VALUE-TRIPLE (QUOTE DEF-RULESET))))) (18 RECORD-EXPANSION (DEFSECTION ADD-TO-RULESET :PARENTS (RULESETS) :SHORT "@(call add-to-ruleset) adds additional rules to an existing
ruleset." :LONG "<p>Examples:</p>
@({
 (add-to-ruleset my-rules
   '(foop))

 (add-to-ruleset other-rules
   '(car-cons cdr-cons (force)))
})" (DEFMACRO ADD-TO-RULESET (NAME FORM) (DECLARE (XARGS :GUARD (SYMBOLP NAME))) (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE WORLD) (CONS (CONS (QUOTE W) (CONS (QUOTE STATE) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE NAME) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE ER-PROGN) (CONS (CONS (QUOTE CHECK-RULESET) (CONS (QUOTE NAME) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL))))) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE RULES) (CONS (RULESET-FORM-PREPROCESS FORM) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE ADD-TO-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE ADD-TO-RULESET)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO ADD-TO-RULESET (NAME FORM) (DECLARE (XARGS :GUARD (SYMBOLP NAME))) (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE WORLD) (CONS (CONS (QUOTE W) (CONS (QUOTE STATE) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE NAME) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE ER-PROGN) (CONS (CONS (QUOTE CHECK-RULESET) (CONS (QUOTE NAME) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL))))) (CONS (CONS (QUOTE LET) (CONS (CONS (CONS (QUOTE RULES) (CONS (RULESET-FORM-PREPROCESS FORM) (QUOTE NIL))) (QUOTE NIL)) (CONS (CONS (QUOTE ADD-TO-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))) (QUOTE NIL)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE ADD-TO-RULESET)) (XDOC::PARENTS (QUOTE (RULESETS))) (XDOC::SHORT (QUOTE "@(call add-to-ruleset) adds additional rules to an existing
ruleset.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE ADD-TO-RULESET))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Examples:</p>
@({
 (add-to-ruleset my-rules
   '(foop))

 (add-to-ruleset other-rules
   '(car-cons cdr-cons (force)))
})") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . ADD-TO-RULESET) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RULESETS) (:SHORT . "@(call add-to-ruleset) adds additional rules to an existing
ruleset.") (:LONG . "<p>Examples:</p>
@({
 (add-to-ruleset my-rules
   '(foop))

 (add-to-ruleset other-rules
   '(car-cons cdr-cons (force)))
})

") (:FROM . "[books]/tools/rulesets.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC ADD-TO-RULESET)))))) (VALUE-TRIPLE (QUOTE ADD-TO-RULESET))))) (19 RECORD-EXPANSION (DEFSECTION DEF-RULESET! :PARENTS (RULESETS) :SHORT "Same as @(see def-ruleset) except that it overwrites any already
existing ruleset instead of causing an error." (DEFMACRO DEF-RULESET! (NAME FORM) (DECLARE (XARGS :GUARD (SYMBOLP NAME))) (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE LET*) (CONS (CONS (CONS (QUOTE WORLD) (CONS (CONS (QUOTE W) (CONS (QUOTE STATE) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE NAME) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE RULES) (CONS (RULESET-FORM-PREPROCESS FORM) (QUOTE NIL))) (QUOTE NIL)))) (CONS (CONS (QUOTE IF) (CONS (CONS (QUOTE IS-RULESET) (CONS (QUOTE NAME) (CONS (QUOTE WORLD) (QUOTE NIL)))) (CONS (CONS (QUOTE ADD-TO-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (CONS (CONS (QUOTE DEF-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (QUOTE NIL))))) (QUOTE NIL)))) (QUOTE NIL))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE DEF-RULESET!)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO DEF-RULESET! (NAME FORM) (DECLARE (XARGS :GUARD (SYMBOLP NAME))) (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE LET*) (CONS (CONS (CONS (QUOTE WORLD) (CONS (CONS (QUOTE W) (CONS (QUOTE STATE) (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE NAME) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (QUOTE NIL))) (CONS (CONS (QUOTE RULES) (CONS (RULESET-FORM-PREPROCESS FORM) (QUOTE NIL))) (QUOTE NIL)))) (CONS (CONS (QUOTE IF) (CONS (CONS (QUOTE IS-RULESET) (CONS (QUOTE NAME) (CONS (QUOTE WORLD) (QUOTE NIL)))) (CONS (CONS (QUOTE ADD-TO-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (CONS (CONS (QUOTE DEF-RULESET-CORE) (CONS (QUOTE NAME) (CONS (QUOTE RULES) (CONS (QUOTE WORLD) (CONS (QUOTE STATE) (QUOTE NIL)))))) (QUOTE NIL))))) (QUOTE NIL)))) (QUOTE NIL)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE DEF-RULESET!)) (XDOC::PARENTS (QUOTE (RULESETS))) (XDOC::SHORT (QUOTE "Same as @(see def-ruleset) except that it overwrites any already
existing ruleset instead of causing an error.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE DEF-RULESET!))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . DEF-RULESET!) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RULESETS) (:SHORT . "Same as @(see def-ruleset) except that it overwrites any already
existing ruleset instead of causing an error.") (:LONG . "

") (:FROM . "[books]/tools/rulesets.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC DEF-RULESET!)))))) (VALUE-TRIPLE (QUOTE DEF-RULESET!))))) (24 RECORD-EXPANSION (DEFSECTION ENABLE* :PARENTS (RULESETS) :SHORT "Ruleset-aware version of @(see enable)." :LONG "<p>Examples:</p>

@({
 (in-theory (enable* my-rules append car-cons))

 (defthm ...
    :hints ((\"Goal\" :in-theory (enable* foo ...))))
})" (DEFMACRO ENABLE* (&REST X) (CONS (QUOTE UNION-THEORIES-FN) (CONS (CONS (QUOTE CURRENT-THEORY) (CONS (QUOTE :HERE) (QUOTE NIL))) (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS X (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (CONS (QUOTE T) (CONS (QUOTE WORLD) (QUOTE NIL)))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE ENABLE*)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO ENABLE* (&REST X) (CONS (QUOTE UNION-THEORIES-FN) (CONS (CONS (QUOTE CURRENT-THEORY) (CONS (QUOTE :HERE) (QUOTE NIL))) (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS X (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (CONS (QUOTE T) (CONS (QUOTE WORLD) (QUOTE NIL))))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE ENABLE*)) (XDOC::PARENTS (QUOTE (RULESETS))) (XDOC::SHORT (QUOTE "Ruleset-aware version of @(see enable).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE ENABLE*))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Examples:</p>

@({
 (in-theory (enable* my-rules append car-cons))

 (defthm ...
    :hints ((\"Goal\" :in-theory (enable* foo ...))))
})") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . ENABLE*) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RULESETS) (:SHORT . "Ruleset-aware version of @(see enable).") (:LONG . "<p>Examples:</p>

@({
 (in-theory (enable* my-rules append car-cons))

 (defthm ...
    :hints ((\"Goal\" :in-theory (enable* foo ...))))
})

") (:FROM . "[books]/tools/rulesets.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC ENABLE*)))))) (VALUE-TRIPLE (QUOTE ENABLE*))))) (25 RECORD-EXPANSION (DEFSECTION DISABLE* :PARENTS (RULESETS) :SHORT "Ruleset-aware version of @(see disable)." :LONG "<p>Examples:</p>

@({
 (in-theory (disable* my-rules append car-cons))

 (defthm ...
    :hints ((\"Goal\" :in-theory (disable* foo ...))))
})" (DEFMACRO DISABLE* (&REST X) (CONS (QUOTE SET-DIFFERENCE-THEORIES-FN) (CONS (CONS (QUOTE CURRENT-THEORY) (CONS (QUOTE :HERE) (QUOTE NIL))) (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS X (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (CONS (QUOTE T) (CONS (QUOTE WORLD) (QUOTE NIL)))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE DISABLE*)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO DISABLE* (&REST X) (CONS (QUOTE SET-DIFFERENCE-THEORIES-FN) (CONS (CONS (QUOTE CURRENT-THEORY) (CONS (QUOTE :HERE) (QUOTE NIL))) (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS X (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (CONS (QUOTE T) (CONS (QUOTE WORLD) (QUOTE NIL))))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE DISABLE*)) (XDOC::PARENTS (QUOTE (RULESETS))) (XDOC::SHORT (QUOTE "Ruleset-aware version of @(see disable).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE DISABLE*))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Examples:</p>

@({
 (in-theory (disable* my-rules append car-cons))

 (defthm ...
    :hints ((\"Goal\" :in-theory (disable* foo ...))))
})") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . DISABLE*) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RULESETS) (:SHORT . "Ruleset-aware version of @(see disable).") (:LONG . "<p>Examples:</p>

@({
 (in-theory (disable* my-rules append car-cons))

 (defthm ...
    :hints ((\"Goal\" :in-theory (disable* foo ...))))
})

") (:FROM . "[books]/tools/rulesets.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC DISABLE*)))))) (VALUE-TRIPLE (QUOTE DISABLE*))))) (26 RECORD-EXPANSION (DEFSECTION E/D* :PARENTS (RULESETS) :SHORT "Ruleset-aware version of @(see e/d)." :LONG "<p>Examples:</p>

@({
 (in-theory (e/d* (unusual-rules append)
                  (expensive-rules default-car default-cdr)))

 (defthm ...
    :hints ((\"Goal\"
             :in-theory (e/d* (unusual-rules append)
                              (expensive-rules default-car
                               default-cdr)))))
})" (DEFUN E/D*-FN (THEORY E/D-LIST ENABLE-P) (DECLARE (XARGS :GUARD (AND (TRUE-LIST-LISTP E/D-LIST) (OR (EQ ENABLE-P T) (EQ ENABLE-P NIL))))) (COND ((ATOM E/D-LIST) THEORY) (ENABLE-P (E/D*-FN (CONS (QUOTE UNION-THEORIES) (CONS THEORY (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS (CAR E/D-LIST) (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (QUOTE NIL)))) (CDR E/D-LIST) NIL)) (T (E/D*-FN (CONS (QUOTE SET-DIFFERENCE-THEORIES) (CONS THEORY (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS (CAR E/D-LIST) (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (QUOTE NIL)))) (CDR E/D-LIST) T)))) (DEFMACRO E/D** (&REST THEORIES) (DECLARE (XARGS :GUARD (TRUE-LIST-LISTP THEORIES))) (COND ((ATOM THEORIES) NIL) (T (E/D*-FN NIL THEORIES T)))) (DEFMACRO E/D* (&REST THEORIES) (DECLARE (XARGS :GUARD (TRUE-LIST-LISTP THEORIES))) (COND ((ATOM THEORIES) (QUOTE (CURRENT-THEORY :HERE))) (T (E/D*-FN (QUOTE (CURRENT-THEORY :HERE)) THEORIES T))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE E/D*)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUN E/D*-FN (THEORY E/D-LIST ENABLE-P) (DECLARE (XARGS :GUARD (AND (TRUE-LIST-LISTP E/D-LIST) (OR (EQ ENABLE-P T) (EQ ENABLE-P NIL))))) (COND ((ATOM E/D-LIST) THEORY) (ENABLE-P (E/D*-FN (CONS (QUOTE UNION-THEORIES) (CONS THEORY (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS (CAR E/D-LIST) (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (QUOTE NIL)))) (CDR E/D-LIST) NIL)) (T (E/D*-FN (CONS (QUOTE SET-DIFFERENCE-THEORIES) (CONS THEORY (CONS (CONS (QUOTE EXPAND-RULESET) (CONS (CONS (QUOTE QUOTE) (CONS (CAR E/D-LIST) (QUOTE NIL))) (CONS (QUOTE WORLD) (QUOTE NIL)))) (QUOTE NIL)))) (CDR E/D-LIST) T)))) (DEFMACRO E/D** (&REST THEORIES) (DECLARE (XARGS :GUARD (TRUE-LIST-LISTP THEORIES))) (COND ((ATOM THEORIES) NIL) (T (E/D*-FN NIL THEORIES T)))) (DEFMACRO E/D* (&REST THEORIES) (DECLARE (XARGS :GUARD (TRUE-LIST-LISTP THEORIES))) (COND ((ATOM THEORIES) (QUOTE (CURRENT-THEORY :HERE))) (T (E/D*-FN (QUOTE (CURRENT-THEORY :HERE)) THEORIES T)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE E/D*)) (XDOC::PARENTS (QUOTE (RULESETS))) (XDOC::SHORT (QUOTE "Ruleset-aware version of @(see e/d).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE E/D*))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Examples:</p>

@({
 (in-theory (e/d* (unusual-rules append)
                  (expensive-rules default-car default-cdr)))

 (defthm ...
    :hints ((\"Goal\"
             :in-theory (e/d* (unusual-rules append)
                              (expensive-rules default-car
                               default-cdr)))))
})") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . E/D*) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RULESETS) (:SHORT . "Ruleset-aware version of @(see e/d).") (:LONG . "<p>Examples:</p>

@({
 (in-theory (e/d* (unusual-rules append)
                  (expensive-rules default-car default-cdr)))

 (defthm ...
    :hints ((\"Goal\"
             :in-theory (e/d* (unusual-rules append)
                              (expensive-rules default-car
                               default-cdr)))))
})

<h3>Definitions and Theorems</h3>@(def |ACL2|::|E/D*-FN|)") (:FROM . "[books]/tools/rulesets.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC E/D*)))))) (VALUE-TRIPLE (QUOTE E/D*))))))
NIL
(("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573))
358963686

APT Browse - Built by Thomas Orozco.