+/** Specialization of symbol to real domain */
+class realsymbol : public symbol
+{
+ // constructors
+public:
+ realsymbol();
+ explicit realsymbol(const std::string & initname, unsigned domain = domain::real);
+ realsymbol(const std::string & initname, const std::string & texname, unsigned domain = domain::real);
+ realsymbol(const std::string & initname, unsigned rt, unsigned rtt, unsigned domain = domain::real);
+ realsymbol(const std::string & initname, const std::string & texname, unsigned rt, unsigned rtt, unsigned domain = domain::real);
+};
+