# [isabelle] Problems with Real addition

Hi,
I'm trying out addition in Real, but have run into some problems. Does
anyone know why the first example below doesn't work but the second does? Is
it a problem with the types?
1)
theory Test
imports Real
begin
typedecl T
consts
F :: "T => real"
t :: "T"
axioms
ax : "F(t) = 0"
lemma test: "EX x. F(x) + 1 ~= 0"
using ax
by auto
2)
theory Test
imports Real
begin
typedecl T
consts
F :: "T => real"
t :: "T"
axioms
ax : "F(t) = 0"
lemma test: "EX x. F(x) + 0 = 0"
using ax
by auto
Thanks in advance for any help.
Regards,
Steve

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*