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