doc-src/TutorialI/Ifexpr/Ifexpr.thy
changeset 13790 8d7e9fce8c50
parent 12327 5a4d78204492
child 15243 ba52fdc2c4e8
equal deleted inserted replaced
13789:d37f66755f47 13790:8d7e9fce8c50