# HG changeset patch
# User huffman
# Date 1287687829 25200
# Node ID 54159b52f3392238b6d59695c2e6df67d881bf12
# Parent  f4be971c574648535615d0aa922c287849bb4d97
rename lemma spair_lemma to spair_Sprod

diff -r f4be971c5746 -r 54159b52f339 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Oct 21 06:03:18 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Thu Oct 21 12:03:49 2010 -0700
@@ -27,9 +27,6 @@
 type_notation (HTML output)
   sprod  ("(_ \<otimes>/ _)" [21,20] 20)
 
-lemma spair_lemma: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> Sprod"
-by (simp add: Sprod_def strict_conv_if)
-
 subsection {* Definitions of constants *}
 
 definition
@@ -59,15 +56,14 @@
 
 subsection {* Case analysis *}
 
+lemma spair_Sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> Sprod"
+by (simp add: Sprod_def strict_conv_if)
+
 lemma spair_Abs_Sprod: "(:a, b:) = Abs_Sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
-by (simp add: spair_def cont_Abs_Sprod spair_lemma)
+by (simp add: spair_def cont_Abs_Sprod spair_Sprod)
 
 lemma Rep_Sprod_spair: "Rep_Sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
-by (simp add: spair_Abs_Sprod Abs_Sprod_inverse spair_lemma)
-
-lemmas Rep_Sprod_simps =
-  Rep_Sprod_inject [symmetric] below_Sprod_def
-  Rep_Sprod_strict Rep_Sprod_spair
+by (simp add: spair_Abs_Sprod Abs_Sprod_inverse spair_Sprod)
 
 lemma sprodE [case_names bottom spair, cases type: sprod]:
   obtains "p = \<bottom>" | x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>"
@@ -80,6 +76,10 @@
 
 subsection {* Properties of \emph{spair} *}
 
+lemmas Rep_Sprod_simps =
+  Rep_Sprod_inject [symmetric] below_Sprod_def
+  Rep_Sprod_strict Rep_Sprod_spair
+
 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
 by (simp add: Rep_Sprod_simps strict_conv_if)