| #
200df247 |
|
01-Apr-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Define < as an abbrevation using <=. Start theory of ordinals.
Only got as far as showing that the Nats are well-ordered.
Note that the well-order conjunct requires existence of *least* elements,
not minimal ones, as per the standard HOL def'n of WF.
|