Quelle  ROOT

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_Term_Typing
    Grounded_Selection_Function
    IsaFoR_KBO
    IsaFoR_Nonground_Clause
    IsaFoR_Nonground_Clause_With_Equality
    IsaFoR_Ground_Critical_Pairs
    Monomorphic_Typing
    Nonground_Entailment
    Nonground_Inference
    Nonground_Order
    Nonground_Order_With_Equality
    Nonground_Typing
    Nonground_Typing_With_Equality
    Typed_Substitution_Example
    Typed_Substitution_Lifting_Example
    Typed_Tiebreakers
    Untyped_Calculus
  document_files
    "root.tex"