doc-src/TutorialI/Misc/Option2.thy
changeset 10950 aa788fcb75a5
parent 10561 d960cc4a6afc
child 11310 51e70b7bc315