| changeset 65449 | c82e63b11b8b |
| parent 61798 | 27f3c10b0b50 |
| child 76213 | e44d86131648 |
--- a/src/ZF/Induct/ListN.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/ListN.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \<open>Lists of n elements\<close> -theory ListN imports Main begin +theory ListN imports ZF begin text \<open> Inductive definition of lists of \<open>n\<close> elements; see