src/HOL/Library/Case_Converter.thy
changeset 78861 5c91bd51fc37
parent 77811 ae9e6218443d