src/Doc/Tutorial/Misc/Plus.thy
changeset 80870 9a7de3f320d8
parent 67613 ce654b0e6d69