Re: [isabelle] Occur Check Problem in Isabelle

Dear Anja,

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
Computational Logic Group
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

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