src/Doc/Tutorial/Ifexpr/Ifexpr.thy
changeset 69497 c434ca819aea
parent 67613 ce654b0e6d69
child 69505 cc2d676d5395