doc-src/TutorialI/Misc/case_exprs.thy
changeset 27809 a1e409db516b
parent 25340 6a3b20f0ae61
equal deleted inserted replaced
27808:4dd3d5efcc7f 27809:a1e409db516b