equal
deleted
inserted
replaced
9 is not a limit ordinal? |
9 is not a limit ordinal? |
10 *) |
10 *) |
11 |
11 |
12 header{*Quine-Inspired Ordered Pairs and Disjoint Sums*} |
12 header{*Quine-Inspired Ordered Pairs and Disjoint Sums*} |
13 |
13 |
14 theory QPair = Sum + mono: |
14 theory QPair = Sum + func: |
15 |
15 |
16 text{*For non-well-founded data |
16 text{*For non-well-founded data |
17 structures in ZF. Does not precisely follow Quine's construction. Thanks |
17 structures in ZF. Does not precisely follow Quine's construction. Thanks |
18 to Thomas Forster for suggesting this approach! |
18 to Thomas Forster for suggesting this approach! |
19 |
19 |