Re: [isabelle] Occur Check Problem in Isabelle
you might also have a look at IsaFoR at
It contains several formalizations about terms and term rewriting, including a fully formalized unification algorithm for first order terms (theory Substitution.thy).
Am 16.07.2011 um 22:48 schrieb Anja Gerbes:
> Good evening,
> I can not prove the lemma, however.
> Can you tell me how I should do in the proof of the
> lemma continues to Isabelle runs through here?
> Thank you in advance
> Anja Gerbes
> datatype 'a trm = Var 'a | Fn 'a "('a
> trm) list"
> types 'a subst = "('a \<times> 'a trm) list"
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
This archive was generated by a fusion of
Pipermail (Mailman edition) and