doc-src/TutorialI/Misc/Option2.thy
changeset 47871 861dc9184920
parent 36176 3fe7e97ccca8
equal deleted inserted replaced
47870:ec815d64573f 47871:861dc9184920