src/Doc/Tutorial/Misc/Itrev.thy
changeset 80870 9a7de3f320d8
parent 69597 ff784d5a5bfb