src/Doc/Tutorial/Misc/Option2.thy
changeset 67948 83902fff6243
parent 67406 23307fd33906
child 69505 cc2d676d5395