changed if_bool_eq to if_bool_eq_conj
authorpaulson
Thu Apr 02 13:48:48 1998 +0200 (1998-04-02)
changeset 47703e026ace28da
parent 4769 bb60149fe21b
child 4771 f1bacbbe02a8
changed if_bool_eq to if_bool_eq_conj
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Thu Apr 02 13:48:28 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Apr 02 13:48:48 1998 +0200
     1.3 @@ -654,7 +654,7 @@
     1.4  bind_thm ("expand_if_mem2", 
     1.5      read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if);
     1.6  
     1.7 -val expand_ifs = [if_bool_eq, expand_if_eq1, expand_if_eq2,
     1.8 +val expand_ifs = [if_bool_eq_conj, expand_if_eq1, expand_if_eq2,
     1.9  		  expand_if_mem1, expand_if_mem2];
    1.10  
    1.11