[isabelle-dev] NEWS

Lawrence Paulson lp15 at cam.ac.uk
Thu Sep 17 16:04:07 CEST 2009

NEWS * New method metisFT: A version of metis that uses full type  
in order to avoid failures of proof reconstruction.

It hasn't been tested much. Ultimately, the idea is to incorporate it  
into Metis itself so that it is called automatically if the untyped  
version raises an exception.


More information about the isabelle-dev mailing list