src/Doc/Tutorial/Misc/Option2.thy
changeset 70006 f12a52b5d812
parent 69597 ff784d5a5bfb