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. "