Re: [isabelle] The syntactic equality

On 27.06.2012 04:31, Shuling Wang wrote:

I need to define the syntax substitution of terms in Isabelle/HOL. So first, for two terms of real, how can I define the syntactic equality?
For example, x::real, y::real, we need to have "x not equal y".
Or are there already good solutions for syntax substitution in Isabelle?

If you want to do reasoning on the syntax of terms, you need to use a deep embedding. I.e. define your own datatype to represent terms and reason then on the structure of this datatype.

  -- Lars

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