src/Doc/Locales/Examples1.thy
changeset 74971 16eaa56f69f7
parent 69597 ff784d5a5bfb