src/HOL/ex/LocaleGroup.ML
changeset 9195 29f1e53f9937
parent 6024 cb87f103d114