Re: [isabelle] union-find based unification


The union-find structures are in the examples folder in

However, someone seems to have messed up ROOT.ML when porting to
Isabelle2013, such that this file is not compiled any more!

I'll check whether Union_Find still compiles under 2013, and send a
patch here if it does not.
Best, and thanks for pointing to the problem,

> which mentions union-find trees in the introduction, but by skimming 
> over the theory names nothing immediately jumped at me ;)
> The reason I ask is for an efficient (code generatable) formalization, 
> using union-find,  of a first-order unification algorithm. Anybody aware 
> that this was already done?
> cheers
> chris

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