# HG changeset patch
# User huffman
# Date 1293133946 28800
# Node ID 1a7557cc686a2a9db62defa0ac9a5f9311c42250
# Parent  ad093e4638e25297aa605620749b6e268e7aabdd
replaced separate lemmas seq{1,2,3} with seq_simps

diff -r ad093e4638e2 -r 1a7557cc686a src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Thu Dec 23 11:51:59 2010 -0800
+++ b/src/HOL/HOLCF/Cfun.thy	Thu Dec 23 11:52:26 2010 -0800
@@ -483,14 +483,11 @@
 lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
 unfolding seq_def by simp
 
-lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
-by (simp add: seq_conv_if)
-
-lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
-by (simp add: seq_conv_if)
-
-lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
-by (simp add: seq_conv_if)
+lemma seq_simps [simp]:
+  "seq\<cdot>\<bottom> = \<bottom>"
+  "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
+by (simp_all add: seq_conv_if)
 
 definition
   strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where