src/Doc/Tutorial/Misc/Option2.thy
changeset 67317 15ea49331fc7
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
67316:adaf279ce67b 67317:15ea49331fc7