src/Doc/Tutorial/Misc/case_exprs.thy
changeset 72133 c500f6c86e86
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
72132:d756ff4bb3a3 72133:c500f6c86e86