Theory HOL_Basics

✐‹creator "Kevin Kappelmann"›
section ‹HOL-Basics›
theory HOL_Basics
  imports
    LBinary_Relations
    LFunctions
    Galois
    Orders
    Predicates
begin

paragraph ‹Summary›
text ‹Library on top of HOL axioms, as required for Transport \<^cite>‹"transport"›.
Requires ∗‹only› the HOL axioms, nothing else.
Includes:
▸ Basic concepts on binary relations, relativised properties,
  and restricted equalities e.g. @{term "left_total_on"} and @{term "eq_restrict"}.
▸ Basic concepts on functions, relativised properties, and relators,
  e.g. @{term "injective_on"} and @{term "dep_mono_wrt_pred"}.
▸ Basic concepts on orders and relativised order-theoretic properties,
  e.g. @{term "partial_equivalence_rel_on"}.
▸ Galois connections, Galois equivalences, order equivalences, and
  other related concepts on order functors,
  e.g. @{term "galois.galois_equivalence"}.
▸ Basic concepts on predicates.
▸ Syntax bundles for HOL @{dir "HOL_Syntax_Bundles"}.
▸ Alignments for concepts that have counterparts in the HOL library -
  see @{dir "HOL_Alignments"}.›

end