| changeset 4770 | 3e026ace28da |
| parent 4686 | 74a12e86b20b |
| child 4830 | bd73675adbed |
--- a/src/HOL/Set.ML Thu Apr 02 13:48:28 1998 +0200 +++ b/src/HOL/Set.ML Thu Apr 02 13:48:48 1998 +0200 @@ -654,7 +654,7 @@ bind_thm ("expand_if_mem2", read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if); -val expand_ifs = [if_bool_eq, expand_if_eq1, expand_if_eq2, +val expand_ifs = [if_bool_eq_conj, expand_if_eq1, expand_if_eq2, expand_if_mem1, expand_if_mem2];