# [isabelle] Syntax for existential equation

Hi,
Is the following using the correct syntax for existential equation? I found
it somewhere, but ProofGeneral seems to not like it.
axioms ga_function_monotonicity_25 [rule_format] :
"ALL x1.
ALL x2. gn_inj_Nat_Int(x1) mod' gn_inj_Nat_Int(x2) =e= x1 mod'' x2"
*** Type unification failed: Clash of types "*" and "bool"
*** Type error in application: Incompatible operand type
***
*** Operator: op = (gn_inj_Nat_Int(x1) mod' gn_inj_Nat_Int(x2) = e) :: bool
=> bool
*** Operand: x1 mod'' x2 :: bool * X_Nat
***
*** The error(s) above occurred in axiom "ga_function_monotonicity_25"
*** At command "axioms".
It seems that the 'e' in =e= is parsed as a variable.
Thanks.
Michael

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