doc-src/TutorialI/Misc/case_exprs.thy
changeset 33875 e5e7faaed7ad
parent 25340 6a3b20f0ae61
equal deleted inserted replaced
33874:1db5ca5eadf5 33875:e5e7faaed7ad