#
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.
|