src/HOL/ex/Locales.thy
changeset 23817 ee3ee9ea0d34
parent 19931 fb32b43e7f80