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