1 | ;; find-theorems.el A search form for Isabelle's find_theorems command. |
---|
2 | ;; |
---|
3 | ;; Copyright (C) 2007 Tjark Weber <tjark.weber@gmx.de> |
---|
4 | ;; |
---|
5 | ;; This program is free software; you can redistribute it and/or |
---|
6 | ;; modify it under the terms of the GNU General Public License |
---|
7 | ;; as published by the Free Software Foundation; either version 2 |
---|
8 | ;; of the License, or (at your option) any later version. |
---|
9 | ;; |
---|
10 | ;; $Id: find-theorems.el,v 1.1 2007/05/10 22:41:15 da Exp $ |
---|
11 | ;; |
---|
12 | |
---|
13 | ;; make the original (minibuffer based) "Find theorems" command (from |
---|
14 | ;; ../generic/pg-user.el) available as proof-find-theorems-minibuffer; |
---|
15 | ;; return '(nil) so that proof-find-theorems-minibuffer works as a |
---|
16 | ;; value for proof-find-theorems-command |
---|
17 | |
---|
18 | (defun proof-find-theorems-minibuffer () |
---|
19 | "Search for items containing given constants (using the minibuffer)." |
---|
20 | (interactive) |
---|
21 | (let ((proof-find-theorems-command "find_theorems %s")) |
---|
22 | (call-interactively 'proof-find-theorems)) |
---|
23 | '(nil)) |
---|
24 | |
---|
25 | ;; proof-find-theorems-form (just like proof-find-theorems-minibuffer) can be |
---|
26 | ;; called interactively, and can be used as a value for |
---|
27 | ;; proof-find-theorems-command (returning '(nil) means that the actual |
---|
28 | ;; "find_theorems" command will NOT be issued to Isabelle by |
---|
29 | ;; proof-find-theorems in this case, but only later on by a handler function |
---|
30 | ;; for the form's "Find" button) |
---|
31 | |
---|
32 | (defun proof-find-theorems-form () |
---|
33 | "Search for items containing given constants (using a search form)." |
---|
34 | (interactive) |
---|
35 | (apply 'proof-find-theorems-create-searchform proof-find-theorems-data) |
---|
36 | '(nil)) |
---|
37 | |
---|
38 | ;; update the universal key bindings (see ../generic/proof-config.el) |
---|
39 | ;; |
---|
40 | ;; C-c C-a C-m is bound to proof-find-theorems-minibuffer |
---|
41 | ;; C-c C-a C-f is bound to proof-find-theorems-form |
---|
42 | ;; |
---|
43 | ;; Note that C-c C-a C-f, although C-c C-a usually invokes the prover |
---|
44 | ;; assistant specific keymap, is defined as a universal key binding here. |
---|
45 | ;; This way it will be available in the same buffers as C-c C-f. |
---|
46 | |
---|
47 | (setq proof-universal-keys |
---|
48 | (cons |
---|
49 | '([(control c) (control a) (control m)] . proof-find-theorems-minibuffer) |
---|
50 | (cons |
---|
51 | '([(control c) (control a) (control f)] . proof-find-theorems-form) |
---|
52 | proof-universal-keys))) |
---|
53 | |
---|
54 | ;; Documentation, taken from isabelle/NEWS: |
---|
55 | ;; |
---|
56 | ;; * Command 'find_theorems' searches for a list of criteria instead of a |
---|
57 | ;; list of constants. Known criteria are: intro, elim, dest, name:string, |
---|
58 | ;; simp:term, and any term. Criteria can be preceded by '-' to select |
---|
59 | ;; theorems that do not match. Intro, elim, dest select theorems that |
---|
60 | ;; match the current goal, name:s selects theorems whose fully qualified |
---|
61 | ;; name contain s, and simp:term selects all simplification rules whose |
---|
62 | ;; lhs match term. Any other term is interpreted as pattern and selects |
---|
63 | ;; all theorems matching the pattern. Available in ProofGeneral under |
---|
64 | ;; 'ProofGeneral -> Find Theorems' or C-c C-f. Example: |
---|
65 | ;; |
---|
66 | ;; C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL." |
---|
67 | ;; |
---|
68 | ;; prints the last 100 theorems matching the pattern "(_::nat) + _ + _", |
---|
69 | ;; matching the current goal as introduction rule and not having "HOL." |
---|
70 | ;; in their name (i.e. not being defined in theory HOL). |
---|
71 | |
---|
72 | ;; search form field values |
---|
73 | |
---|
74 | (defvar proof-find-theorems-data (list |
---|
75 | "" ;; num |
---|
76 | "" ;; pattern |
---|
77 | "none" ;; intro |
---|
78 | "none" ;; elim |
---|
79 | "none" ;; dest |
---|
80 | "" ;; name |
---|
81 | "" ;; simp |
---|
82 | ) |
---|
83 | "Values of the Find Theorems search form's fields.") |
---|
84 | |
---|
85 | ;; search form widgets (set in proof-find-theorems-create-searchform |
---|
86 | ;; and accessed in the "Find" handler) |
---|
87 | |
---|
88 | (defvar proof-find-theorems-widget-number nil |
---|
89 | "Search form widget for the number of theorems.") |
---|
90 | |
---|
91 | (defvar proof-find-theorems-widget-pattern nil |
---|
92 | "Search form widget for search patterns.") |
---|
93 | |
---|
94 | (defvar proof-find-theorems-widget-intro nil |
---|
95 | "Search form widget for intro rules.") |
---|
96 | |
---|
97 | (defvar proof-find-theorems-widget-elim nil |
---|
98 | "Search form widget for elim rules.") |
---|
99 | |
---|
100 | (defvar proof-find-theorems-widget-dest nil |
---|
101 | "Search form widget for dest rules.") |
---|
102 | |
---|
103 | (defvar proof-find-theorems-widget-name nil |
---|
104 | "Search form widget for theorem names.") |
---|
105 | |
---|
106 | (defvar proof-find-theorems-widget-simp nil |
---|
107 | "Search form widget for simplification rules.") |
---|
108 | |
---|
109 | ;; creates (or switches to) the search form buffer |
---|
110 | |
---|
111 | (defun proof-find-theorems-create-searchform |
---|
112 | (num pattern intro elim dest name simp &optional errmsg) |
---|
113 | "Create (or switch to) the Find Theorems search form buffer." |
---|
114 | |
---|
115 | (if (get-buffer "*Find Theorems*") |
---|
116 | (switch-to-buffer "*Find Theorems*") |
---|
117 | |
---|
118 | ;; create a new search form |
---|
119 | |
---|
120 | (switch-to-buffer "*Find Theorems*") |
---|
121 | |
---|
122 | (widget-insert |
---|
123 | (concat "\n " (propertize "Find Theorems" |
---|
124 | 'face (list :height 200 :weight 'extra-bold)) |
---|
125 | "\n\n")) |
---|
126 | |
---|
127 | ;; pattern |
---|
128 | (widget-insert " Search pattern: ") |
---|
129 | (setq proof-find-theorems-widget-pattern (widget-create 'editable-field |
---|
130 | :size 50 |
---|
131 | :help-echo "A pattern to match in the theorem." |
---|
132 | pattern)) |
---|
133 | (widget-insert " ") |
---|
134 | (widget-create 'push-button |
---|
135 | :help-echo "Click <mouse-2> for help." |
---|
136 | :notify (lambda (&rest ignore) (proof-find-theorems-create-help)) |
---|
137 | "?") |
---|
138 | |
---|
139 | ;; name |
---|
140 | (widget-insert "\n\n Theorem name: ") |
---|
141 | (setq proof-find-theorems-widget-name (widget-create 'editable-field |
---|
142 | :size 50 |
---|
143 | :help-echo "Part of the theorem's name." |
---|
144 | name)) |
---|
145 | (widget-insert " ") |
---|
146 | (widget-create 'push-button |
---|
147 | :help-echo "Click <mouse-2> for help." |
---|
148 | :notify (lambda (&rest ignore) (proof-find-theorems-create-help)) |
---|
149 | "?") |
---|
150 | |
---|
151 | ;; intro |
---|
152 | (widget-insert "\n\n Rules matching the current goal: ") |
---|
153 | (widget-create 'push-button |
---|
154 | :help-echo "Click <mouse-2> for help." |
---|
155 | :notify (lambda (&rest ignore) (proof-find-theorems-create-help)) |
---|
156 | "?") |
---|
157 | (widget-insert "\n\n INTRO:\n ") |
---|
158 | (setq proof-find-theorems-widget-intro (widget-create 'radio-button-choice |
---|
159 | :value intro |
---|
160 | :indent 6 |
---|
161 | :button-args (list :help-echo "Click <mouse-2> to select one option.") |
---|
162 | '(item "none") '(item "intro") '(item "-intro"))) |
---|
163 | |
---|
164 | ;; elim |
---|
165 | (widget-insert "\n ELIM:\n ") |
---|
166 | (setq proof-find-theorems-widget-elim (widget-create 'radio-button-choice |
---|
167 | :value elim |
---|
168 | :indent 6 |
---|
169 | :button-args (list :help-echo "Click <mouse-2> to select one option.") |
---|
170 | '(item "none") '(item "elim") '(item "-elim"))) |
---|
171 | |
---|
172 | ;; dest |
---|
173 | (widget-insert "\n DEST:\n ") |
---|
174 | (setq proof-find-theorems-widget-dest (widget-create 'radio-button-choice |
---|
175 | :value dest |
---|
176 | :indent 6 |
---|
177 | :button-args (list :help-echo "Click <mouse-2> to select one option.") |
---|
178 | '(item "none") '(item "dest") '(item "-dest"))) |
---|
179 | |
---|
180 | ;; simp |
---|
181 | (widget-insert "\n Simplification pattern: ") |
---|
182 | (setq proof-find-theorems-widget-simp (widget-create 'editable-field |
---|
183 | :size 42 |
---|
184 | :help-echo |
---|
185 | "A pattern to match in the left-hand side of a simplification rule." |
---|
186 | simp)) |
---|
187 | (widget-insert " ") |
---|
188 | (widget-create 'push-button |
---|
189 | :help-echo "Click <mouse-2> for help." |
---|
190 | :notify (lambda (&rest ignore) (proof-find-theorems-create-help)) |
---|
191 | "?") |
---|
192 | |
---|
193 | ;; num |
---|
194 | (widget-insert "\n\n Number of results: ") |
---|
195 | (setq proof-find-theorems-widget-number (widget-create 'editable-field |
---|
196 | :size 10 |
---|
197 | :help-echo "Maximum number of results to be displayed." |
---|
198 | num)) |
---|
199 | (widget-insert " ") |
---|
200 | (widget-create 'push-button |
---|
201 | :help-echo "Click <mouse-2> for help." |
---|
202 | :notify (lambda (&rest ignore) (proof-find-theorems-create-help)) |
---|
203 | "?") |
---|
204 | |
---|
205 | ;; Find |
---|
206 | (widget-insert "\n\n ") |
---|
207 | (widget-create 'push-button |
---|
208 | :help-echo "Click <mouse-2> to submit this form." |
---|
209 | :notify (lambda (&rest ignore) |
---|
210 | (let ((num (widget-value proof-find-theorems-widget-number)) |
---|
211 | (pattern (widget-value proof-find-theorems-widget-pattern)) |
---|
212 | (intro (widget-value proof-find-theorems-widget-intro)) |
---|
213 | (elim (widget-value proof-find-theorems-widget-elim)) |
---|
214 | (dest (widget-value proof-find-theorems-widget-dest)) |
---|
215 | (name (widget-value proof-find-theorems-widget-name)) |
---|
216 | (simp (widget-value proof-find-theorems-widget-simp))) |
---|
217 | (kill-buffer "*Find Theorems*") |
---|
218 | (proof-find-theorems-submit-searchform |
---|
219 | num pattern intro elim dest name simp))) |
---|
220 | "Find") |
---|
221 | |
---|
222 | ;; Reset form |
---|
223 | (widget-insert " ") |
---|
224 | (widget-create 'push-button |
---|
225 | :help-echo "Click <mouse-2> to reset this form." |
---|
226 | :notify (lambda (&rest ignore) |
---|
227 | (kill-buffer "*Find Theorems*") |
---|
228 | (proof-find-theorems-create-searchform |
---|
229 | "" "" "none" "none" "none" "" "")) |
---|
230 | "Reset Form") |
---|
231 | (widget-insert "\n") |
---|
232 | |
---|
233 | ;; errmsg |
---|
234 | (if errmsg |
---|
235 | (widget-insert (concat "\n " (propertize |
---|
236 | (concat errmsg "\n See help for details.") |
---|
237 | 'face (list :foreground "red")) "\n"))) |
---|
238 | |
---|
239 | (use-local-map widget-keymap) |
---|
240 | (widget-setup) |
---|
241 | |
---|
242 | (goto-char 37)) ;; beginning of the "Search pattern" text field |
---|
243 | ) |
---|
244 | |
---|
245 | ;; creates the search form help buffer |
---|
246 | |
---|
247 | (defun proof-find-theorems-create-help () |
---|
248 | "Create a help text buffer for the Find Theorems search form." |
---|
249 | |
---|
250 | (with-output-to-temp-buffer "*Find Theorems - Help*" |
---|
251 | (princ (concat |
---|
252 | "\n" |
---|
253 | "*** Find Theorems - Help ***\n" |
---|
254 | "\n" |
---|
255 | "Command \"Find Theorems\" (C-c C-f) searches for theorems that satisfy a list of\n" |
---|
256 | "user-supplied criteria. Known criteria are:\n" |
---|
257 | "\n" |
---|
258 | "* Search pattern: a pattern that occurs in the theorem, e.g. \"(_::nat) + _\".\n" |
---|
259 | "\n" |
---|
260 | "* Theorem name: a substring of the theorem's fully qualified name. (Treats \"*\"\n" |
---|
261 | " as a wildcard character.)\n" |
---|
262 | "\n" |
---|
263 | "* Intro, Elim, Dest: select theorems that match the current goal as\n" |
---|
264 | " introduction/elimination/destruction rule.\n" |
---|
265 | "\n" |
---|
266 | "* Simplification pattern: selects simplification rules whose left-hand side\n" |
---|
267 | " matches the given pattern.\n" |
---|
268 | "\n" |
---|
269 | "* Number of results: an upper bound on the number of theorems that are\n" |
---|
270 | " displayed. (Leave empty to use Isabelle's default value.)\n" |
---|
271 | "\n" |
---|
272 | "Multiple search patterns, theorem names and simplification patterns can be\n" |
---|
273 | "given, separated by spaces. (Patterns containing a space must be enclosed in\n" |
---|
274 | "double-quotes.) Criteria can be preceded by \"-\" to select theorems that do not.\n" |
---|
275 | "match. (Patterns that begin with a \"-\" must be enclosed in double-quotes.)\n" |
---|
276 | "\n" |
---|
277 | "A minibuffer based \"Find Theorems\" command is available via (C-c C-a C-m). See\n" |
---|
278 | "the Isabelle NEWS file for up-to-date documentation. A search form is available\n" |
---|
279 | "via (C-c C-a C-f). Variable proof-find-theorems-command (customizable via\n" |
---|
280 | "Proof-General > Advanced > Internals > Prover Config) controls the default\n" |
---|
281 | "behavior of the \"Find Theorems\" command: set to proof-find-theorems-form or\n" |
---|
282 | "proof-find-theorems-minibuffer.\n" |
---|
283 | ))) |
---|
284 | ) |
---|
285 | |
---|
286 | ;; parses the search form's data and calls proof-find-theorems |
---|
287 | ;; with an appropriate argument string, or displays the search |
---|
288 | ;; form again, but with an error message |
---|
289 | |
---|
290 | (defun proof-find-theorems-submit-searchform |
---|
291 | (num pattern intro elim dest name simp) |
---|
292 | "Parse the Find Theorems search form's data." |
---|
293 | |
---|
294 | (let (num_ pattern_ intro_ elim_ dest_ name_ simp_ searchstring) |
---|
295 | |
---|
296 | ;; pattern |
---|
297 | (setq pattern_ (proof-find-theorems-parse-criteria "" pattern)) |
---|
298 | |
---|
299 | (if (not (pop pattern_)) |
---|
300 | (proof-find-theorems-create-searchform |
---|
301 | num pattern intro elim dest name simp |
---|
302 | (concat "Invalid search pattern: " (car pattern_))) |
---|
303 | |
---|
304 | (setq pattern_ (car pattern_)) |
---|
305 | |
---|
306 | ;; name |
---|
307 | (setq name_ (proof-find-theorems-parse-criteria "name: " name)) |
---|
308 | |
---|
309 | (if (not (pop name_)) |
---|
310 | (proof-find-theorems-create-searchform |
---|
311 | num pattern intro elim dest name simp |
---|
312 | (concat "Invalid theorem name: " (car name_))) |
---|
313 | |
---|
314 | (setq name_ (car name_)) |
---|
315 | |
---|
316 | ;; simp |
---|
317 | (setq simp_ (proof-find-theorems-parse-criteria "simp: " simp)) |
---|
318 | |
---|
319 | (if (not (pop simp_)) |
---|
320 | (proof-find-theorems-create-searchform |
---|
321 | num pattern intro elim dest name simp |
---|
322 | (concat "Invalid simplification pattern: " (car simp_))) |
---|
323 | |
---|
324 | (setq simp_ (car simp_)) |
---|
325 | |
---|
326 | ;; num |
---|
327 | (setq num_ (proof-find-theorems-parse-number num)) |
---|
328 | |
---|
329 | (if (not num_) |
---|
330 | (proof-find-theorems-create-searchform |
---|
331 | num pattern intro elim dest name simp |
---|
332 | "Number of results must be a positive integer.") |
---|
333 | |
---|
334 | ;; intro |
---|
335 | (setq intro_ (if (equal intro "none") "" intro)) |
---|
336 | |
---|
337 | ;; elim |
---|
338 | (setq elim_ (if (equal elim "none") "" elim)) |
---|
339 | |
---|
340 | ;; dest |
---|
341 | (setq dest_ (if (equal dest "none") "" dest)) |
---|
342 | |
---|
343 | ;; success: save data, call proof-find-theorems |
---|
344 | (setq proof-find-theorems-data |
---|
345 | (list num pattern intro elim dest name simp)) |
---|
346 | |
---|
347 | (setq searchstring (format "find_theorems %s" |
---|
348 | (mapconcat 'identity |
---|
349 | (proof-find-theorems-filter-empty |
---|
350 | (list num_ pattern_ intro_ elim_ dest_ name_ simp_)) |
---|
351 | " "))) |
---|
352 | |
---|
353 | ;; note that proof-find-theorems with an argument provided |
---|
354 | ;; will merely pass this on to Isabelle, and NOT display |
---|
355 | ;; the search form again |
---|
356 | (proof-find-theorems searchstring)))))) |
---|
357 | ) |
---|
358 | |
---|
359 | ;; "Multiple search patterns, theorem names and simplification terms can be |
---|
360 | ;; given, separated by spaces. (Patterns containing a space must be enclosed |
---|
361 | ;; in double-quotes.) Criteria can be preceded by "-" to select theorems that |
---|
362 | ;; do not match. (Patterns that begin with a "-" must be enclosed in double- |
---|
363 | ;; quotes.)" |
---|
364 | ;; |
---|
365 | ;; returns (t parsed-string) (where parsed-string may be empty) or |
---|
366 | ;; (nil errmsg) in case of an error |
---|
367 | |
---|
368 | (defun proof-find-theorems-parse-criteria (option-string criteria-string) |
---|
369 | "Parse search patterns/theorem names/simplification terms, |
---|
370 | separated by \" \", possibly preceded by \"-\", and possibly |
---|
371 | escaped by double-quotes." |
---|
372 | |
---|
373 | ;; This code might benefit greatly from the use of regexps. |
---|
374 | |
---|
375 | (let ((tokens nil) (errmsg nil)) |
---|
376 | |
---|
377 | ;; turn criteria-string into a list of (string) tokens |
---|
378 | (while (and (not (equal criteria-string "")) (not errmsg)) |
---|
379 | |
---|
380 | ;; ignore space |
---|
381 | (if (equal (elt criteria-string 0) ?\ ) |
---|
382 | (setq criteria-string (substring criteria-string 1)) |
---|
383 | |
---|
384 | ;; - is a token |
---|
385 | ;; Note: This is still a bit weird, as it treats a - following a - |
---|
386 | ;; just like the first -, i.e. not as part of a pattern. Oh |
---|
387 | ;; well. |
---|
388 | (if (equal (elt criteria-string 0) ?-) |
---|
389 | (progn |
---|
390 | (setq tokens (cons "-" tokens)) |
---|
391 | (setq criteria-string (substring criteria-string 1))) |
---|
392 | |
---|
393 | ;; " starts a token: search for the next ", regard as one token |
---|
394 | ;; Note: This is still a bit weird, as it does not require the |
---|
395 | ;; closing double-quotes to be followed by a space. Oh well. |
---|
396 | (if (equal (elt criteria-string 0) ?\") |
---|
397 | (let ((i 1)) |
---|
398 | (while (and (< i (length criteria-string)) |
---|
399 | (not (equal (elt criteria-string i) ?\"))) |
---|
400 | (setq i (1+ i))) |
---|
401 | (if (equal i (length criteria-string)) |
---|
402 | (setq errmsg "missing closing double-quotes.") |
---|
403 | (setq i (1+ i)) |
---|
404 | (setq tokens (cons (substring criteria-string 0 i) tokens)) |
---|
405 | (setq criteria-string (substring criteria-string i)))) |
---|
406 | |
---|
407 | ;; everything else: search for the next space, regard as one token |
---|
408 | ;; Note: This is still a bit weird, as it scans over double-quotes. |
---|
409 | ;; Oh well. |
---|
410 | (let ((i 1)) |
---|
411 | (while (and (< i (length criteria-string)) |
---|
412 | (not (equal (elt criteria-string i) ?\ ))) |
---|
413 | (setq i (1+ i))) |
---|
414 | (setq tokens (cons (substring criteria-string 0 i) tokens)) |
---|
415 | (setq criteria-string (substring criteria-string i))) |
---|
416 | ))) |
---|
417 | ) |
---|
418 | |
---|
419 | (if errmsg |
---|
420 | (list nil errmsg) |
---|
421 | |
---|
422 | (setq tokens (nreverse tokens)) |
---|
423 | |
---|
424 | ;; convert the tokens into argument strings; make sure every "-" is |
---|
425 | ;; followed by a pattern/name (i.e. not by another "-") |
---|
426 | (let ((strings nil) (negated nil)) |
---|
427 | |
---|
428 | (while (and tokens (not errmsg)) |
---|
429 | (let ((token (car tokens))) |
---|
430 | (if (equal token "-") |
---|
431 | (if negated |
---|
432 | (setq errmsg "- may not be followed by another -.") |
---|
433 | (setq negated t) |
---|
434 | (setq tokens (cdr tokens))) |
---|
435 | (setq strings (cons |
---|
436 | (concat (if negated "-" "") option-string |
---|
437 | ;; wrap token in double-quotes if necessary |
---|
438 | (if (equal (elt token 0) ?\") token (concat "\"" token "\""))) |
---|
439 | strings)) |
---|
440 | (setq negated nil) |
---|
441 | (setq tokens (cdr tokens)))) |
---|
442 | ) |
---|
443 | |
---|
444 | (if errmsg |
---|
445 | (list nil errmsg) |
---|
446 | |
---|
447 | (if negated |
---|
448 | (list nil "- must be followed by a search criterion.") |
---|
449 | |
---|
450 | (setq strings (nreverse strings)) |
---|
451 | |
---|
452 | (list t (mapconcat 'identity strings " ")) |
---|
453 | ))))) |
---|
454 | ) |
---|
455 | |
---|
456 | ;; auxiliary functions |
---|
457 | |
---|
458 | ;; returns "" if num is "", "(num)" if num is a string encoding a positive |
---|
459 | ;; integer, and nil otherwise |
---|
460 | |
---|
461 | (defun proof-find-theorems-parse-number (num) |
---|
462 | "Parse the number of theorems to be displayed." |
---|
463 | (if (equal num "") |
---|
464 | "" |
---|
465 | (let ((numval (string-to-number num))) |
---|
466 | (if (and (wholenump numval) (not (equal numval 0))) |
---|
467 | (concat "(" (number-to-string numval) ")") |
---|
468 | nil))) |
---|
469 | ) |
---|
470 | |
---|
471 | (defun proof-find-theorems-filter-empty (strings) |
---|
472 | "Build a new list by removing empty strings from a (non-circular) list." |
---|
473 | (if (not strings) |
---|
474 | nil |
---|
475 | (if (equal (car strings) "") |
---|
476 | (proof-find-theorems-filter-empty (cdr strings)) |
---|
477 | (cons (car strings) |
---|
478 | (proof-find-theorems-filter-empty (cdr strings))))) |
---|
479 | ) |
---|
480 | |
---|
481 | (provide 'find-theorems) |
---|