doc-src/TutorialI/Misc/case_exprs.thy
changeset 10795 9e888d60d3e5
parent 10420 ef006735bee8
child 10824 4a212e635318