[acl2/acl2] 634a57: For hol-in-acl2 library: tweaked eval_poly example...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 634a57fd1ab0c1d6f7033494101f4783a11fa5e3
https://github.com/acl2/acl2/commit/634a57fd1ab0c1d6f7033494101f4783a11fa5e3
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-12 (Mon, 12 Jan 2026)

Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp

Log Message:
-----------
For hol-in-acl2 library: tweaked eval_poly example, and changed ex1 example to be much more interesting.

Thanks to Konrad Slind for running the translator to get this
extension of the ex1 example.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing

[Pete Manolios]

Branch: refs/heads/testing-acl2s