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

Larry



More information about the isabelle-dev mailing list