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