session Superposition_Calculus_Rest = Saturation_Framework_Extensions +
  sessions
    Knuth_Bendix_Order
    Min_Max_Least_Greatest
    Regular_Tree_Relations
    Saturation_Framework
    Saturation_Framework_Extensions
    Abstract_Substitution
    Superposition_Calculus

  theories (* Rest that did not make it into the Afp. *)
    Fun_Extra
    Renaming

  theories (* This theory contains an analogue specification of ground ordered resolution. *)
    Ground_Ordered_Resolution

session Ground_Critical_Pairs_Theorem in Ground_Critical_Pairs_Theorem = Superposition_Calculus +
  description "This theory contains a proof of the ground critical-pair assumption found in some locales of the session Superposition_Calculus. It should not be submitted to the AFP in the same entry due to LGPL conflict."
  sessions
    "HOL-Library"
    Superposition_Calculus
  theories
    LGPL_Ground_Critical_Pairs_Adapted_From_CeTA
