Entry | Value |
---|---|
Name | MAX |
Conclusion | !m n. MAX m n = (if m <= n then n else m) |
Constructive Proof | Yes |
Axiom | N|A |
Classical Lemmas | N|A |
Constructive Lemmas | |
Contained Package | natural-order-min-max-def |
Comment | Standard HOL library retrieved from OpenTheory |