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

[Lawrence Paulson]

Metis also relies on clause form.
Larry

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>