(* Title: HOL/Library/Simps_Case_Conv.thy Author: Lars Noschinski *) theory Simps_Case_Conv imports Case_Converter keywords "simps_of_case" "case_of_simps" :: thy_decl abbrevs "simps_of_case" "case_of_simps" = "" begin ML_file \<open>simps_case_conv.ML\<close> end