src/HOL/Product_Type.thy
changeset 26798 a9134a089106
parent 26588 d83271bfaba5
child 26975 103dca19ef2e
     1.1 --- a/src/HOL/Product_Type.thy	Wed May 07 10:56:39 2008 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed May 07 10:56:40 2008 +0200
     1.3 @@ -476,7 +476,7 @@
     1.4  Addsimprocs [split_beta_proc, split_eta_proc];
     1.5  *}
     1.6  
     1.7 -lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
     1.8 +lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
     1.9    by (subst surjective_pairing, rule split_conv)
    1.10  
    1.11  lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"