| changeset 65449 | c82e63b11b8b |
| parent 61980 | 6b780867d426 |
| child 76213 | e44d86131648 |
--- a/src/ZF/Induct/Brouwer.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Brouwer.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \<open>Infinite branching datatype definitions\<close> -theory Brouwer imports Main_ZFC begin +theory Brouwer imports ZFC begin subsection \<open>The Brouwer ordinals\<close>