include "Q/q/qtimes.ma".
include "Q/q/qplus.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
-notation "\rationals" non associative with precedence 99 for @{'q}.
-interpretation "Q" 'q = Q.
+interpretation "Q" 'Q = Q.
(* group over Q *)
axiom qp : ℚ → ℚ → ℚ.