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