doc-src/TutorialI/Misc/case_exprs.thy
changeset 45124 d78ec6c10fa1
parent 25340 6a3b20f0ae61
equal deleted inserted replaced
45122:49e305100097 45124:d78ec6c10fa1