# HG changeset patch
# User huffman
# Date 1287752094 25200
# Node ID 1b5f394866d9862506f9b774f561a4b5c633b6ce
# Parent  c339c0e8fdfb71c35ad108a9662b7f39bca1b9d7
simplify proof

diff -r c339c0e8fdfb -r 1b5f394866d9 src/HOLCF/FOCUS/Fstream.thy
--- 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"