src/Doc/Locales/Examples1.thy
changeset 75424 5f8f0bf8c72c
parent 69597 ff784d5a5bfb