# HG changeset patch
# User paulson
# Date 891517728 -7200
# Node ID 3e026ace28dacc9c4c8cb73c36004d999c3c224f
# Parent  bb60149fe21b585eb3a79643f3db970df7cd7a9c
changed if_bool_eq to if_bool_eq_conj

diff -r bb60149fe21b -r 3e026ace28da src/HOL/Set.ML
--- 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];