src/Doc/Locales/Examples1.thy
changeset 80847 93c2058896a4
parent 69597 ff784d5a5bfb