[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Christian Sternagel wrote:

>> 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 ;)

For the formalization part, the one who is actually doing it is by 
definition the "proving expert".  After some decades of prover technology 
built around these former core parts of Isabelle, it should be more 
feasible than ever before.

What happens at the moment is just the usual attempt to get existing ML 
modules in a slightly better form, without breaking down completely.


 	Makarius