doc-src/TutorialI/Ifexpr/Ifexpr.thy
changeset 14610 9c2e31e483b2
parent 12327 5a4d78204492
child 15243 ba52fdc2c4e8
equal deleted inserted replaced
14609:663e0e435866 14610:9c2e31e483b2