equal
deleted
inserted
replaced
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 Description : Explicit construction of hypernaturals using |
4 Description : Explicit construction of hypernaturals using |
5 ultrafilters |
5 ultrafilters |
6 *) |
6 *) |
7 |
7 |
|
8 (* blast confuses different versions of < *) |
|
9 DelIffs [order_less_irrefl]; |
|
10 Addsimps [order_less_irrefl]; |
|
11 |
8 (*------------------------------------------------------------------------ |
12 (*------------------------------------------------------------------------ |
9 Properties of hypnatrel |
13 Properties of hypnatrel |
10 ------------------------------------------------------------------------*) |
14 ------------------------------------------------------------------------*) |
11 |
15 |
12 (** Proving that hyprel is an equivalence relation **) |
16 (** Proving that hyprel is an equivalence relation **) |