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