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