[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

Lawrence Paulson lp15 at cam.ac.uk
Fri Sep 14 16:23:13 CEST 2007

Metis also relies on clause form.

On 14 Sep 2007, at 15:21, Florian Haftmann wrote:

> I must confess that I have lost track now.  Does only the  
> skolemization
> depend on Hilbert-Choice, or also metis?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070914/a2a179fa/attachment.html>

More information about the isabelle-dev mailing list