# HG changeset patch
# User huffman
# Date 1203528496 -3600
# Node ID 2ae572207783e9c67986df2772b9d08d747e44cd
# Parent  a657683e902af6b700f840c2606d20bdf45fcb3f
fix proofs involving ile_def

diff -r a657683e902a -r 2ae572207783 src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Wed Feb 20 14:52:38 2008 +0100
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Wed Feb 20 18:28:16 2008 +0100
@@ -54,7 +54,7 @@
 apply (subst slen_infinite)
 apply (erule thin_rl)
 apply (drule spec)
-apply (fold ile_def)
+apply (unfold linorder_not_less)
 apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
 apply (simp)
 done
@@ -142,7 +142,7 @@
 apply (erule conjE)
 apply (case_tac "#x < Fin i")
 apply ( fast)
-apply (fold ile_def)
+apply (unfold linorder_not_less)
 apply (drule (1) mp)
 apply (erule all_dupE, drule mp, rule refl_less)
 apply (erule ssubst)
diff -r a657683e902a -r 2ae572207783 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Wed Feb 20 14:52:38 2008 +0100
+++ b/src/HOLCF/ex/Stream.thy	Wed Feb 20 18:28:16 2008 +0100
@@ -433,7 +433,7 @@
 by (simp add: inat_defs split:inat_splits)
 
 lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
-by (simp add: ile_def slen_take_eq)
+by (simp add: linorder_not_less [symmetric] slen_take_eq)
 
 lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
 by (rule slen_take_eq_rev [THEN iffD1], auto)