doc-src/TutorialI/Misc/case_exprs.thy
changeset 13790 8d7e9fce8c50
parent 12699 deae80045527
child 16417 9bc16273c2d4
equal deleted inserted replaced
13789:d37f66755f47 13790:8d7e9fce8c50