| changeset 68490 | eb53f944c8cd |
| parent 67443 | 3abf6a722518 |
| child 69593 | 3dda49e08b9d |
--- a/src/ZF/Zorn.thy Sun Jun 24 11:41:41 2018 +0100 +++ b/src/ZF/Zorn.thy Sun Jun 24 15:57:48 2018 +0200 @@ -5,7 +5,7 @@ section\<open>Zorn's Lemma\<close> -theory Zorn imports OrderArith AC Inductive_ZF begin +theory Zorn imports OrderArith AC Inductive begin text\<open>Based upon the unpublished article ``Towards the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.\<close>