Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 228:49736efc822b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
try transfinite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2019 20:42:48 +0900
parents 176ff97547b4
children e06b76e5b682
comparison
equal deleted inserted replaced
227:a4cdfc84f65f 228:49736efc822b
481 Union = ZF.Union OD→ZF 481 Union = ZF.Union OD→ZF
482 Power = ZF.Power OD→ZF 482 Power = ZF.Power OD→ZF
483 Select = ZF.Select OD→ZF 483 Select = ZF.Select OD→ZF
484 Replace = ZF.Replace OD→ZF 484 Replace = ZF.Replace OD→ZF
485 isZF = ZF.isZF OD→ZF 485 isZF = ZF.isZF OD→ZF
486 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)