src/Doc/Tutorial/Misc/Option2.thy
changeset 59660 49e498cedd02
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
59657:2441a80fb6c1 59660:49e498cedd02