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