src/HOL/ex/Locales.thy
changeset 14024 213dcc39358f
parent 13538 359c085c4def
child 14254 342634f38451