theory Refine_Lib imports Refine_Util Attr_Comb Named_Sorted_Thms Prio_List Mpat_Antiquot Mk_Term_Antiquot Tagged_Solver Anti_Unification Misc Foldi Indep_Vars Select_Solve Mk_Record_Simp begin ML_file "Cond_Rewr_Conv.ML" ML_file "Revert_Abbrev.ML" end