changeset 68490 | eb53f944c8cd |
parent 65464 | f3cd78ba687c |
child 69587 | 53982d5ec0bb |
--- a/src/ZF/ZF.thy Sun Jun 24 11:41:41 2018 +0100 +++ b/src/ZF/ZF.thy Sun Jun 24 15:57:48 2018 +0200 @@ -1,6 +1,6 @@ section\<open>Main ZF Theory: Everything Except AC\<close> -theory ZF imports List_ZF IntDiv_ZF CardinalArith begin +theory ZF imports List IntDiv CardinalArith begin (*The theory of "iterates" logically belongs to Nat, but can't go there because primrec isn't available into after Datatype.*)