doc-src/TutorialI/Misc/case_exprs.thy
changeset 12434 ff2efde4574d
parent 11457 279da0358aa9
child 12699 deae80045527
equal deleted inserted replaced
12433:654acbf26fcc 12434:ff2efde4574d