# 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\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\x = x" by (rule slen_take_eq_rev [THEN iffD1], auto)