src/Doc/Tutorial/Misc/Option2.thy
changeset 64612 08e4b1aeac50
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
64611:d72d63d05bdb 64612:08e4b1aeac50