Mercurial > hg > Members > kono > Proof > ZF-in-agda
log ordinal.agda @ 229:5e36744b8dce
age | author | description |
---|---|---|
2019-08-10 | Shinji KONO | recover ε-induction |
2019-08-09 | Shinji KONO | TransFinite induction fixed |
2019-08-07 | Shinji KONO | try to separate Ordinals |
2019-08-06 | Shinji KONO | try func |
2019-08-02 | Shinji KONO | separate logic and nat |
2019-07-31 | Shinji KONO | Transfinite induction fixed |
2019-07-31 | Shinji KONO | fixing transfinte induction... |
2019-07-30 | Shinji KONO | ε-induction like loop again |
2019-07-22 | Shinji KONO | ... |
2019-07-21 | Shinji KONO | fix zf |
2019-07-20 | Shinji KONO | new ordinal-definable |
2019-07-18 | Shinji KONO | ... |
2019-07-17 | Shinji KONO | use double negation |
2019-07-16 | Shinji KONO | minor fix |
2019-07-14 | Shinji KONO | Union trans finite |
2019-07-08 | Shinji KONO | ... |
2019-07-08 | Shinji KONO | Union again |
2019-07-08 | Shinji KONO | Power Set |
2019-07-02 | Shinji KONO | ord power set |
2019-07-01 | Shinji KONO | ... |
2019-06-25 | Shinji KONO | ... |
2019-06-20 | Shinji KONO | ... |
2019-06-09 | Shinji KONO | power set using sup on Def |
2019-06-08 | Shinji KONO | ... |
2019-06-05 | Shinji KONO | infinity axiom done |
2019-06-05 | Shinji KONO | osuc work around done |
2019-06-04 | Shinji KONO | split omax? |
2019-06-04 | Shinji KONO | internal error |
2019-06-04 | Shinji KONO | omax-induction does not work |
2019-06-04 | Shinji KONO | omax .. |
2019-06-03 | Shinji KONO | simpler ordinal |
2019-06-02 | Shinji KONO | Union done |
2019-06-01 | Shinji KONO | ordinal atomical successor? |
2019-06-01 | Shinji KONO | fix ordinal |
2019-06-01 | Shinji KONO | ... |
2019-06-01 | Shinji KONO | add osuc ( next larger element of Ordinal ) |
2019-06-01 | Shinji KONO | Union needs +1 space |
2019-05-25 | Shinji KONO | == and ∅7 |
2019-05-24 | Shinji KONO | equalitu and internal parametorisity |
2019-05-23 | Shinji KONO | mnimul |
2019-05-23 | Shinji KONO | ... |
2019-05-22 | Shinji KONO | ordinal fixed |
2019-05-22 | Shinji KONO | fix oridinal |
2019-05-21 | Shinji KONO | fix |
2019-05-21 | Shinji KONO | oridnal dead end |
2019-05-21 | Shinji KONO | fix ordinal |
2019-05-20 | Shinji KONO | problem on Ordinal ( OSuc ℵ ) |
2019-05-20 | Shinji KONO | posturate OD is isomorphic to Ordinal base constructible-set.agda@7e901a899f88 |