# HG changeset patch
# User huffman
# Date 1118182588 -7200
# Node ID 17db5df51a3544adbcfc86ddf630bedc9d1f8140
# Parent  bfb2f513916a3b1d703debc80363ef7856ad4894
renamed theorems less_ssum4a,b,c,d to more meaningful names

diff -r bfb2f513916a -r 17db5df51a35 src/HOLCF/Ssum.ML
--- a/src/HOLCF/Ssum.ML	Wed Jun 08 00:07:46 2005 +0200
+++ b/src/HOLCF/Ssum.ML	Wed Jun 08 00:16:28 2005 +0200
@@ -17,18 +17,20 @@
 val noteq_sinlsinr = thm "noteq_sinlsinr";
 val sinl_inject = thm "sinl_inject";
 val sinr_inject = thm "sinr_inject";
+val sinl_eq = thm "sinl_eq";
+val sinr_eq = thm "sinr_eq";
 val sinl_defined = thm "sinl_defined";
 val sinr_defined = thm "sinr_defined";
 val Exh_Ssum1 = thm "Exh_Ssum1";
 val ssumE = thm "ssumE";
 val ssumE2 = thm "ssumE2";
+val sinl_less = thm "sinl_less";
+val sinr_less = thm "sinr_less";
+val sinl_less_sinr = thm "sinl_less_sinr";
+val sinr_less_sinl = thm "sinr_less_sinl";
 val sscase1 = thm "sscase1";
 val sscase2 = thm "sscase2";
 val sscase3 = thm "sscase3";
-val less_ssum4a = thm "less_ssum4a";
-val less_ssum4b = thm "less_ssum4b";
-val less_ssum4c = thm "less_ssum4c";
-val less_ssum4d = thm "less_ssum4d";
 val sscase4 = thm "sscase4";
 val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined,
                 sscase1, sscase2, sscase3];
diff -r bfb2f513916a -r 17db5df51a35 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Jun 08 00:07:46 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Wed Jun 08 00:16:28 2005 +0200
@@ -145,16 +145,16 @@
 
 subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
 
-lemma less_ssum4a: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
+lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less)
 
-lemma less_ssum4b: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
+lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: less_ssum_def Rep_Ssum_sinr cpair_less)
 
-lemma less_ssum4c: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
+lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
 by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
 
-lemma less_ssum4d: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
+lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
 by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
 
 subsection {* Chains of strict sums *}
@@ -162,15 +162,15 @@
 lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
 apply (rule_tac p=p in ssumE)
 apply (rule_tac x="\<bottom>" in exI, simp)
-apply (simp add: less_ssum4a sinl_eq)
-apply (simp add: less_ssum4d)
+apply (simp add: sinl_less sinl_eq)
+apply (simp add: sinr_less_sinl)
 done
 
 lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
 apply (rule_tac p=p in ssumE)
 apply (rule_tac x="\<bottom>" in exI, simp)
-apply (simp add: less_ssum4c)
-apply (simp add: less_ssum4b sinr_eq)
+apply (simp add: sinl_less_sinr)
+apply (simp add: sinr_less sinr_eq)
 done
 
 lemma ssum_chain_lemma: