src/HOL/Library/simps_case_conv.ML
changeset 58913 5be251101978
parent 58028 e4250d370657
child 58956 a816aa3ff391