src/HOL/Library/case_converter.ML
changeset 69074 787f3db8e313
parent 68301 fb5653a7a879
child 69568 de09a7261120