← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/misc/README

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/misc/README
40
40
 
41
41
===============================================================================
42
42
 
 
43
bash.lisp -- simplification of top-level goal
 
44
 
 
45
If you submit (bash term), you will get back a list of terms produced by the
 
46
ACL2 simplifier.  See the description at the top of bash.lisp for details.
 
47
 
 
48
===============================================================================
 
49
 
43
50
computed-hint.lisp -- examples of computed hints
44
51
 
45
52
===============================================================================
157
164
 
158
165
===============================================================================
159
166
 
 
167
hacker.lisp -- Utilities in support of building ACL2 extensions/modifications
 
168
 
 
169
===============================================================================
 
170
 
160
171
hanoi.lisp -- A solution to the Towers of Hanoi problem
161
172
 
162
173
===============================================================================
292
303
total-order.lisp -- total order for ACL2
293
304
 
294
305
===============================================================================
 
306
 
 
307
transfinite.lisp -- generic proof by strong ordinal induction
 
308
 
 
309
This book presents a way to use functional instantiation to reduce a theorem to
 
310
its inductive step in a proof by transfinite induction.  There is an example in
 
311
the book that shows how this works.
 
312
 
 
313
===============================================================================
 
314
 
 
315
untranslate-patterns.lisp -- simple, pattern-based untranslation for ACL2
 
316
 
 
317
===============================================================================