# 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 \ a\b \ 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"