v1.6.0

• Locales and topological spaces
• Functor category
• Euclidean domains and (extended) Euclidean algorithm
• The quotient ring Z/nZ and the field structure on it for prime n
• Solvers for commutative monoids and rings are implemented in the equation meta
• Extensionality meta
• Structure identity principle meta
• simp_coe meta
• cases meta and improved mcases meta
• unfold and unfold_let metas