src/HOL/Product_Type.thy
changeset 15481 fc075ae929e4
parent 15422 cbdddc0efadf
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Product_Type.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -451,9 +451,7 @@
     1.4  
     1.5  lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
     1.6    -- {* For use with @{text split} and the Simplifier. *}
     1.7 -  apply (subst surjective_pairing)
     1.8 -  apply (subst split_conv, blast)
     1.9 -  done
    1.10 +  by (insert surj_pair [of p], clarify, simp)
    1.11  
    1.12  text {*
    1.13    @{thm [source] split_split} could be declared as @{text "[split]"}