src/HOLCF/IOA/meta_theory/Sequence.thy

--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Feb 08 15:54:01 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Feb 11 12:26:07 2010 -0800
@@ -300,14 +300,11 @@
 done
 
 lemma Cons_not_less_nil: "~a>>s << nil"
-apply (subst Consq_def2)
-apply (rule seq.rews)
-apply (rule Def_not_UU)
+apply (simp add: Consq_def2)
 done
 
 lemma Cons_not_nil: "a>>s ~= nil"
-apply (subst Consq_def2)
-apply (rule seq.rews)
+apply (simp add: Consq_def2)
 done
 
 lemma Cons_not_nil2: "nil ~= a>>s"