src/HOL/Library/Simps_Case_Conv.thy
2013-09-06 wenzelm 2013-09-06 more standard header;
2013-09-06 noschinl 2013-09-06 added simps_of_case and case_of_simps to convert between simps and case rules