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