src/HOL/Library/simps_case_conv.ML
2013-09-06 wenzelm 2013-09-06 more standard header;
2013-09-06 noschinl 2013-09-06 allowed less exhaustive patterns
2013-09-06 noschinl 2013-09-06 added simps_of_case and case_of_simps to convert between simps and case rules