| Entry | Value |
|---|---|
| Name | COND_DEF |
| Conclusion | COND = (\t t1 t2. @x. ((t <=> T) ==> x = t1) /\ ((t <=> F) ==> x = t2)) |
| Constructive Proof | Yes |
| Axiom | N|A |
| Classical Lemmas | N|A |
| Constructive Lemmas | N|A |
| Contained Package | bool-def |
| Comment | Standard HOL library retrieved from OpenTheory |