equal
deleted
inserted
replaced
72 apply ( rule exI) |
72 apply ( rule exI) |
73 apply ( rule slen_strict_mono) |
73 apply ( rule slen_strict_mono) |
74 apply ( erule spec) |
74 apply ( erule spec) |
75 apply ( assumption) |
75 apply ( assumption) |
76 apply ( assumption) |
76 apply ( assumption) |
77 apply (metis inat_ord_code(4) slen_infinite) |
77 apply (metis enat_ord_code(4) slen_infinite) |
78 done |
78 done |
79 |
79 |
80 (* should be without reference to stream length? *) |
80 (* should be without reference to stream length? *) |
81 lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); |
81 lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); |
82 !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P" |
82 !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P" |