doc-src/TutorialI/Misc/Option2.thy
changeset 40434 f775e6e0dc99
parent 36176 3fe7e97ccca8