Real Multiplication does not work
For reasons not obvious to me or @Jazzpirate the rule for real multiplication does not work. We need this for the CICM demo of the MMT / Jupyter paper.
To reproduce this, create a theory T:
theory t : http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics
and then attempt to simplify the term 1.0 \cdot 1.0
.
/cc @frabe @mkohlhase