| Entry | Value |
|---|---|
| Name | LAST |
| Conclusion | !h t. LAST (CONS h t) = (if NULL t then h else LAST t) |
| Constructive Proof | Yes |
| Axiom | N|A |
| Classical Lemmas | N|A |
| Constructive Lemmas | N|A |
| Contained Package | list-last-def |
| Comment | Standard HOL library retrieved from OpenTheory |