HOL icon indicating copy to clipboard operation
HOL copied to clipboard
verified publisher icon HOL-Theorem-Prover

Clean all the various definitions of MAX_LIST

Open ordinarymath opened this issue 7 months ago • 0 comments

There are random redefinitions of MAX_LIST defined in various places. see https://github.com/HOL-Theorem-Prover/HOL/blob/fcb208759e1eb31a235ed87a5dbe5e2bd2fc498b/examples/logic/modal-tableaux/tableauKTScript.sml#L39C1-L42C4

https://github.com/HOL-Theorem-Prover/HOL/blob/fcb208759e1eb31a235ed87a5dbe5e2bd2fc498b/examples/separationLogic/src/treeScript.sml#L266

Note that there's one duplication in holfoot which is fine to keep as its for automation demonstration.

ordinarymath avatar May 06 '25 10:05 ordinarymath