--- a/src/HOL/Main.thy Thu Sep 29 14:15:01 2022 +0200 +++ b/src/HOL/Main.thy Thu Sep 29 14:03:40 2022 +0000 @@ -17,6 +17,7 @@ Conditionally_Complete_Lattices Binomial GCD + Divides begin subsection \<open>Namespace cleanup\<close>