Re: [isabelle] union-find based unification



>    http://afp.sourceforge.net/entries/Separation_Logic_Imperative_HOL.shtml


The union-find structures are in the examples folder in
Examples/Union_Find.thy.

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,
  Peter



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