doc-src/TutorialI/Misc/case_exprs.thy
changeset 12555 e6d7f040fdc7
parent 11457 279da0358aa9
child 12699 deae80045527