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

comparison src/PFOD.agda @ 1293:37f28f427661

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Jun 2023 22:15:17 +0900
parents 45cd80181a29
children ad9ed7c4a0b3
comparison
equal deleted inserted replaced
1292:f29970636e01 1293:37f28f427661
20 20
21 open inOrdinal O 21 open inOrdinal O
22 open OD O 22 open OD O
23 open OD.OD 23 open OD.OD
24 open ODAxiom odAxiom 24 open ODAxiom odAxiom
25 open ODAxiom-ho< odAxiom-ho<
25 import OrdUtil 26 import OrdUtil
26 import ODUtil 27 import ODUtil
27 open Ordinals.Ordinals O 28 open Ordinals.Ordinals O
28 open Ordinals.IsOrdinals isOrdinal 29 open Ordinals.IsOrdinals isOrdinal
29 open Ordinals.IsNext isNext 30 open Ordinals.IsNext isNext