sig
  module type Constructor =
    sig
      val negation : Term.term -> Term.term
      val conjunction : Term.term -> Term.term -> Term.term
      val disjunction : Term.term -> Term.term -> Term.term
      val equivalence : Term.term -> Term.term -> Term.term
      val difference : Term.term -> Term.term -> Term.term
      val implication : Term.term -> Term.term -> Term.term
      val conditional : Term.term -> Term.term -> Term.term -> Term.term
      val equality : Term.term -> Term.term -> Term.term
      val ite : Term.term -> Term.term -> Term.term -> Term.term
    end
  module Standard : Constructor
  module Rbc : Constructor
  module type Rewriter = sig val rewrite : Term.term -> Term.term end
  module Rbc_rewriter : Rewriter
end

---

Hosted by the ^* web site.
^*Other names and brands may be claimed as the property of others.