src/HOL/Library/simps_case_conv.ML
changeset 59882 ada832308efe
parent 59650 ba26118128b7
child 59936 b8ffc3dc9e24