Theory HF_SetCat_Interp

theory HF_SetCat_Interp
imports HF_SetCat
begin

  text‹
    Here we demonstrate the possibility of making a top-level interpretation of
    the ‹ZFC_set_cat› locale.  See theory ‹SetCat_Interp› for further discussion on
    why we do this.
›

  interpretation HF_Sets: hfsetcat .

end