src/HOL/Library/case_converter.ML
13 months ago wenzelm 2018-05-27 prefer existing operation;
13 months ago Andreas Lochbihler 2018-05-12 new tool Code_Lazy