CALL FOR PAPERS AND TUTORIALS
International Conference on Runtime Verification (RV 2010)
November 1 - 4, 2010
Sliema, Malta
http://www.rv2010.org/
Runtime verification (RV) is concerned with monit
On Wednesday 20 January 2010 16:02:10 Roger Bishop Jones wrote:
> On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote:
> > The only relevant information I have come across is Stewart Shapiro's
> > statement, in Foundations without Foundationalism, that in set theory
> > done with second-orde
I once did a proof of the well-ordering principle and several
other Axiom of Choice equivalents (Zorn's Lemma etc.) in HOL88:
http://www.cl.cam.ac.uk/~jrh13/papers/wellorder-library.html
This proof certainly survives in HOL Light (Examples/wo.ml),
and possibly in other versions of HOL too.
F
