# HG changeset patch
# User huffman
# Date 1287787758 25200
# Node ID 0295606b6a36a77056c6be0d17cea218e93b14ff
# Parent  c2d36bc4cd14a1733ce097e3dae81b417c31b47f
rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd

diff -r c2d36bc4cd14 -r 0295606b6a36 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Oct 22 15:47:43 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Fri Oct 22 15:49:18 2010 -0700
@@ -144,7 +144,7 @@
 lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
 by simp
 
-lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
+lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
 by (cases p, simp_all)
 
 lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"