• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
          • Note-2-8
          • Note-2-7
          • Note-8-6
          • Note-8-2
          • Note-7-0
          • Note-8-5
          • Note-8-3
          • Note-8-1
          • Note-8-0
          • Note-7-1
          • Note-6-4
          • Note-2-9-3
          • Note-2-9-1
          • Note-8-4
          • Note-7-2
          • Note-6-5
          • Note-4-0
          • Note-2-9-2
          • Note-3-6
          • Note-3-3
          • Note-3-2-1
          • Note-3-0-1
          • Note-2-9-5
          • Note-2-5
          • Note-1-5
          • Note-6-1
          • Note-4-3
          • Note-4-2
          • Note-4-1
          • Note-3-5
          • Note-3-4
          • Note-3-2
          • Note-3-0-2
          • Note-2-9-4
          • Note-2-9
          • Note-1-8
          • Note-1-7
          • Note-1-6
          • Note-1-4
          • Note-1-3
          • Note-7-4
          • Note-7-3
          • Note-6-3
          • Note-6-2
          • Note-6-0
          • Note-5-0
          • Note-1-9
          • Note-2-2
          • Note-1-8-update
          • Note-3-5(r)
          • Note-2-3
          • Note-3-6-1
          • Release-notes-books
          • Note-1-2
          • Note-2-4
          • Note-2-6
          • Note-2-0
          • Note-3-0
          • Note-3-2(r)
          • Note-2-7(r)
          • Note-1-1
          • Note-3-4(r)
          • Note-3-1
          • Note-2-8(r)
          • Note-2-1
          • Note-2-9(r)
          • Note-2-6(r)
          • Note-3-1(r)
          • Note-3-0(r)
          • Note-3-0-1(r)
          • Note-2-5(r)
          • Note-4-3(r)
          • Note-4-2(r)
          • Note-4-1(r)
          • Note-4-0(r)
          • Note-3-6(r)
          • Note-3-3(r)
          • Note-3-2-1(r)
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Release-notes

Note-1-8-update

ACL2 Version 1.8 (Summer, 1995) Notes

ACL2 can now use Ordered Binary Decision Diagram technology. See bdd. There is also a proof-builder bdd command.

ACL2 is now more respectful of the intention of the function hide. In particular, it is more careful not to dive inside any call of hide during equality substitution and case splitting.

The ld special (see ld) ld-pre-eval-print may now be used to turn off printing of input forms during processing of encapsulate and certify-book forms, by setting it to the value :never, i.e., (set-ld-pre-eval-print :never state). See ld-pre-eval-print.

The TUTORIAL documentation section (now obsolete) has, with much help from Bill Young, been substantially improved to a bona fide introduction.

The term pretty-printer has been modified to introduce (<= X Y) as an abbreviation for (not (< Y X)).

Forward chaining and linear arithmetic now both benefit from the evaluation of ground subterms.

A new macro set-inhibit-output-lst has been defined. This should be used when setting the state global inhibit-output-lst; see set-inhibit-output-lst and see proof-tree.

The test for redundancy in definitions includes the guard and type declarations. See redundant-events.

See generalized-booleans for a discussion of a potential soundness problem for ACL2 related to the question: Which Common Lisp functions are known to return Boolean values?

Here we will put some less important changes, additions, and so on.

A bug has been fixed so that now, execution of :comp t (see comp) correctly handles non-standard characters.

A bug in digit-char-p has been fixed, so that the ``default'' is nil rather than 0.

True-listp now tests the final cdr against nil using eq instead of equal, for improved efficiency. The logical meaning is, however, unchanged.

Put-assoc-equal has been added to the logic (it used to have :defun-mode :program, and has been documented.