src/HOL/ex/LocaleGroup.ML
changeset 6921 78a2ce8fb8df
parent 6024 cb87f103d114