[isabelle] Definition in jEdit

Dear All

I tried to definition the *consts * but it give me error and I do not know
where is it.,,

 Const1:: "type => type"

const_def : " Const1 A = Const1 B ==> A = B"

And the error message is

(((Not a meta-equality (==)
The error(s) above occurred in definition "injective_publicKey":
  "A = B" ))))

Best Regards,

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