Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Zorn's Lemma

Email Gateway (Aug 19 2022 at 09:56):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

where can I get hold of the unpublished article that is mentioned in

http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Zorn.html

The reason for being interested is that I feel the need to modify the
proof of Zorn's lemma in the Library to a version with explicit carrier
sets (in the spirit of my wqo AFP entry).

cheers

chris

Email Gateway (Aug 19 2022 at 09:57):

From: Lawrence Paulson <lp15@cam.ac.uk>
The title of this article is "Towards the Mechanization of the Proofs of some Classical Theorems of Set Theory".

I couldn't find the text on the web. I was given a hard copy by Mike Gordon about 20 years ago.

It is just possible that some of this material was published in the B-Book.

Larry

Last updated: Apr 26 2024 at 20:16 UTC