| changeset 13544 | 895994073bdf |
| parent 13357 | 6f54e992777e |
| child 13780 | af7b79271364 |
--- a/src/ZF/upair.thy Wed Aug 28 13:08:34 2002 +0200 +++ b/src/ZF/upair.thy Wed Aug 28 13:08:50 2002 +0200 @@ -210,6 +210,9 @@ lemma the_eq_trivial [simp]: "(THE x. x = a) = a" by blast +lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a" +by blast + subsection{*Conditional Terms: @{text "if-then-else"}*} lemma if_true [simp]: "(if True then a else b) = a"