changeset 26059 | b67a225b50fd |
parent 26056 | 6a0801279f4c |
child 32960 | 69916a850301 |
--- a/src/ZF/UNITY/Monotonicity.thy Mon Feb 11 21:32:11 2008 +0100 +++ b/src/ZF/UNITY/Monotonicity.thy Mon Feb 11 21:32:12 2008 +0100 @@ -69,7 +69,7 @@ lemma take_mono_left: "[| i le j; xs \<in> list(A); j \<in> nat |] ==> <take(i, xs), take(j, xs)> \<in> prefix(A)" -by (blast intro: Nat_ZF.le_in_nat take_mono_left_lemma) +by (blast intro: le_in_nat take_mono_left_lemma) lemma take_mono_right: "[| <xs,ys> \<in> prefix(A); i \<in> nat |]