[isabelle-dev] auto raises a TYPE exception

Christian Sternagel c.sternagel at gmail.com
Tue May 28 02:32:14 CEST 2013

> Hopefully it is all a bit more precise now.  Maybe someone wants to
> formalize pattern.ML + unify.ML after > 20 years, to pin down the
> remaining uncertaincies about type instantiation within these
> non-trivial algorithms.
Just for the record, I would be interested in joining such an endeavor. 
Unfortunately I'm not a proven expert ;)



More information about the isabelle-dev mailing list