simplify proof

--- a/src/HOLCF/FOCUS/Fstream.thy	Thu Oct 21 15:21:39 2010 -0700
+++ b/src/HOLCF/FOCUS/Fstream.thy	Fri Oct 22 05:54:54 2010 -0700
@@ -42,11 +42,7 @@
 
 
 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
-apply (rule flat_eq [THEN iffD1, symmetric])
-apply (rule Def_not_UU)
-apply (drule antisym_less_inverse)
-apply (erule (1) conjunct2 [THEN trans_less])
-done
+by simp
 
 
 section "fscons"