doc-src/TutorialI/Misc/case_exprs.thy
changeset 28972 cb8a2c3e188f
parent 25340 6a3b20f0ae61
equal deleted inserted replaced
28971:300ec36a19af 28972:cb8a2c3e188f