doc-src/TutorialI/Misc/case_exprs.thy
changeset 29774 829e52cd135d
parent 25340 6a3b20f0ae61
equal deleted inserted replaced
29773:cbaee647ea29 29774:829e52cd135d