ROOT

notable performance tuning (amending a59d9b81be24 and 8976c5bc9e97): avoid costly could_beta_eta_contract, which traverses the whole term;
always use Item_Net.retrieve instead, but on frozen TVars/Vars to enforce matching instead of unification;

chapter_definition HOL
  description "
    Higher-Order Logic.

    Isabelle/HOL is a version of classical higher-order logic resembling
    that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL).
  "

chapter_definition FOL
  description "
    First-Order Logic with some variations: single-sorted vs. many-sorted
    (polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs.
    set-theory (ZF).
  "

chapter_definition Pure
  description "
    The Pure logical framework.

    Isabelle/Pure is a version of intuitionistic higher-order logic that
    expresses rules for Natural Deduction declaratively.
  "

chapter_definition Misc
  description "
    Miscellaneous object-logics, tools, and experiments.
  "

chapter_definition Doc
  description "
    Sources of Documentation.
  "

chapter_definition Unsorted
  description "
    Sessions without 'chapter' declaration.
  "