equal
deleted
inserted
replaced
66 text{*We could probably instantiate some axiomatic type classes and use |
66 text{*We could probably instantiate some axiomatic type classes and use |
67 the standard infix operators.*} |
67 the standard infix operators.*} |
68 |
68 |
69 subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*} |
69 subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*} |
70 |
70 |
71 text{*To define recdef style functions we need an ordering on the Brouwer |
71 text{*To use the function package we need an ordering on the Brouwer |
72 ordinals. Start with a predecessor relation and form its transitive |
72 ordinals. Start with a predecessor relation and form its transitive |
73 closure. *} |
73 closure. *} |
74 |
74 |
75 definition |
75 definition |
76 brouwer_pred :: "(brouwer * brouwer) set" where |
76 brouwer_pred :: "(brouwer * brouwer) set" where |