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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and