src/Doc/Tutorial/Misc/Option2.thy
changeset 71410 5385de42f9f4
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
71409:0bb0cb558bf9 71410:5385de42f9f4