doc-src/TutorialI/Misc/Option2.thy
changeset 10597 29dd6ac8c223
parent 10561 d960cc4a6afc
child 11310 51e70b7bc315