Library Coq.ring.LegacyRing



Require Export Bool.
Require Export LegacyRing_theory.
Require Export Quote.
Require Export Ring_normalize.
Require Export Ring_abstract.


Definition BoolTheory :
  Ring_Theory xorb andb true false (fun b:bool => b) eqb.
Defined.

Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
 [ true false ].