doc-src/TutorialI/Ifexpr/Ifexpr.thy
changeset 14790 0d984ee030a1
parent 12327 5a4d78204492
child 15243 ba52fdc2c4e8
equal deleted inserted replaced
14789:214926b0970c 14790:0d984ee030a1