# HG changeset patch
# User huffman
# Date 1119557250 -7200
# Node ID aa36d41e4263fefb79427735d7ec27f44cc10c75
# Parent  0774e9bcdb6c5c741eec3072b5a60ce0384197c1
add csplit3, ssplit3, fup3 as simp rules

diff -r 0774e9bcdb6c -r aa36d41e4263 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Jun 23 21:27:23 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Thu Jun 23 22:07:30 2005 +0200
@@ -301,7 +301,7 @@
 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
 by (simp add: csplit_def)
 
-lemma csplit3: "csplit\<cdot>cpair\<cdot>z = z"
+lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
 by (simp add: csplit_def surjective_pairing_Cprod2)
 
 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
diff -r 0774e9bcdb6c -r aa36d41e4263 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Jun 23 21:27:23 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Thu Jun 23 22:07:30 2005 +0200
@@ -200,7 +200,7 @@
 lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:)= f\<cdot>x\<cdot>y"
 by (simp add: ssplit_def)
 
-lemma ssplit3: "ssplit\<cdot>spair\<cdot>z = z"
+lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
 by (rule_tac p=z in sprodE, simp_all)
 
 end
diff -r 0774e9bcdb6c -r aa36d41e4263 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Jun 23 21:27:23 2005 +0200
+++ b/src/HOLCF/Up.thy	Thu Jun 23 22:07:30 2005 +0200
@@ -309,7 +309,7 @@
 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 )
 
-lemma fup3: "fup\<cdot>up\<cdot>x = x"
+lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
 by (rule_tac p=x in upE1, simp_all)
 
 end