| changeset 46954 | d8b3412cdb99 |
| parent 46823 | 57bf0cecb366 |
| child 58871 | c399ae4b836f |
--- a/src/ZF/UNITY/AllocBase.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/UNITY/AllocBase.thy Thu Mar 15 17:38:05 2012 +0000 @@ -342,7 +342,7 @@ apply (simp add: length_nat_list_inj) done -lemma nat_lepoll_var: "nat lepoll var" +lemma nat_lepoll_var: "nat \<lesssim> var" apply (unfold lepoll_def) apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI) apply (rule var_infinite_lemma)