src/HOL/Library/simps_case_conv.ML
changeset 58839 ccda99401bc8
parent 58028 e4250d370657
child 58956 a816aa3ff391