chapter AFP
session First_Order_Clause = Abstract_Substitution +
  options [timeout = 900]
  sessions
    Abstract_Substitution
    First_Order_Terms
    Fresh_Identifiers
    "HOL-Cardinals"
    "HOL-Library"
    Min_Max_Least_Greatest
    Nested_Multisets_Ordinals
    "Regular-Sets"
    Regular_Tree_Relations
    Saturation_Framework_Extensions
    Sorted_Terms
    VeriComp
  theories
    Ground_Critical_Pairs
    Ground_Term_Typing
    Grounded_Selection_Function

    Infinite_Variables
    Typed_Tiebreakers
    Untyped_Calculus

    IsaFoR_KBO
    IsaFoR_Nonground_Clause
    IsaFoR_Nonground_Clause_With_Equality
    
    IsaFoR_Ground_Term_Compatibility
    
    Nonground_Entailment
    Nonground_Inference
    Nonground_Order
    Nonground_Order_With_Equality
    Nonground_Typing
    Nonground_Typing_With_Equality

    Polymorphic_Context
    Polymorphic_Term

    Monomorphic_Typing
    Sorted_Terms_Typing

    Typed_Substitution_Example
    Typed_Substitution_Lifting_Example
  document_files
    "root.tex"
