src/Doc/Tutorial/Misc/case_exprs.thy
changeset 66224 9fe05edaa351
parent 58860 fee7cfa69c50
child 67406 23307fd33906