src/HOL/Set.thy
changeset 31197 c1c163ec6c44
parent 31166 a90fe83f58ea
child 31441 428e4caf2299
child 31456 55edadbd43d5
     1.1 --- a/src/HOL/Set.thy	Mon May 18 09:48:06 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon May 18 23:15:38 2009 +0200
     1.3 @@ -1036,11 +1036,16 @@
     1.4  
     1.5  text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
     1.6  
     1.7 -lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})"
     1.8 +lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
     1.9 +by auto
    1.10 +
    1.11 +lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
    1.12  by auto
    1.13  
    1.14 -lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})"
    1.15 -by auto
    1.16 +text {*
    1.17 +Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
    1.18 +to the front (and similarly for @{text "t=x"}):
    1.19 +*}
    1.20  
    1.21  ML{*
    1.22    local
    1.23 @@ -1054,7 +1059,6 @@
    1.24    end;
    1.25  
    1.26    Addsimprocs [defColl_regroup];
    1.27 -
    1.28  *}
    1.29  
    1.30  text {*