src/Doc/Tutorial/Misc/Option2.thy
changeset 59112 e670969f34df
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
59111:c85e018be3a3 59112:e670969f34df