Re: [isabelle] Occur Check Problem in Isabelle



Dear Anja,

you might also have a look at IsaFoR at 
http://cl-informatik.uibk.ac.at/software/ceta/

It contains several formalizations about terms and term rewriting, including a fully formalized unification algorithm for first order terms (theory Substitution.thy).

Cheers,
René

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 MHonArc.