src/Doc/Tutorial/Misc/Option2.thy
changeset 79409 e1895596e1b9
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
79408:d9cf62ea273d 79409:e1895596e1b9