--- 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
--- 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
--- 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