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 begin ML_file "Cond_Rewr_Conv.ML" ML_file "Revert_Abbrev.ML" ML_file "item_net.ML" end