[acl2/acl2] ccfe5e: Fixed defthme macro so that the generated "-forwar...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: ccfe5ef3fa383ab9d4ae2e1c0a07d4e6fc3da601
https://github.com/acl2/acl2/commit/ccfe5ef3fa383ab9d4ae2e1c0a07d4e6fc3da601
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-06-27 (Sat, 27 Jun 2026)

Changed paths:
M books/projects/hol-in-acl2/acl2/hpp-set.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
A books/projects/set-theory/finite/cert.acl2
M books/projects/set-theory/topology/compact-is-normal.lisp
A books/projects/set-theory/topology/compact-is-regular.lisp
M books/projects/set-theory/topology/normal.lisp
M books/projects/set-theory/utilities/defthme.lisp

Log Message:
-----------
Fixed defthme macro so that the generated "-forward" and "-backward" lemmas are disabled. Removed the recent additions of diff$prop to some :props due to one of those lemmas that was formerly enabled.

The lemma (defthme union2-diff-singleton ...) in finite/finite-bang.lisp was
introducing a lemma, union2-diff-singleton-forward, that was needlessly
introducing the need for (diff$prop) hypotheses.



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

[acl2buildserver]

Branch: refs/heads/testing