[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.