src/HOL/Library/simps_case_conv.ML
changeset 58278 e89c7ac4ce16
parent 58028 e4250d370657
child 58956 a816aa3ff391