Object: ho_ml, theory combin
Display form: add_to_simpset `hol_to_nuprl` (hdef_to_simp "ho");; add_info `direct_ old_hdef` `ho`;;
Term structure: add_to_simpset `hol_to_nuprl` (hdef_to_simp "ho");; add_info `direct_old_hdef` `ho`;;