theory Isabelle_2024_Compatibility imports Main "HOL-Library.Multiset" begin lemmas wfP_def = wfp_def lemmas wfP_if_convertible_to_wfP = wfp_if_convertible_to_wfp lemmas wfP_imp_asymp = wfp_imp_asymp lemmas wfP_induct_rule = wfp_induct_rule lemmas wfP_multp = wfp_multp end