Am 01.12.2014 um 03:46 schrieb Waldek Hebisch:
snip
)abbrev domain RR Real
++ Description: The field of real numbers modelled as
++ domain Expression(Integer) + some extensions.
Real : Exports == Implementation where
snip
Exports == FunctionSpace R with
snip
Implementation ==
Kurt Pagani wrote:
Am 25.11.2014 um 20:05 schrieb Waldek Hebisch:
Let me add that assumptions like exements of Expression(Integer)
are real are in general unsound.
Indeed.
In case of log the assumption
is frequently true and not making it would stop useful
simplifications.