| changeset 65449 | c82e63b11b8b |
| parent 61980 | 6b780867d426 |
| child 76213 | e44d86131648 |
--- a/src/ZF/AC.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/AC.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section\<open>The Axiom of Choice\<close> -theory AC imports Main_ZF begin +theory AC imports ZF begin text\<open>This definition comes from Halmos (1960), page 59.\<close> axiomatization where