src/Doc/Tutorial/Misc/Plus.thy
changeset 79586 9cde97e471df
parent 67613 ce654b0e6d69