[isabelle-dev] auto raises a TYPE exception
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