[isabelle-dev] ZF/upair.thy failing

Lawrence Paulson lp15 at cam.ac.uk
Fri Mar 16 11:42:04 CET 2012

Also in ZF/Inductive_ZF.thy...

On 16 Mar 2012, at 10:35, Lawrence Paulson wrote:

> I have a problem with the current version (9ff441f295c2). See attachment. This prevents the use of PG within ZF. However, it builds at the command line. What is supposed to be here?
> <Screen Shot 2012-03-16 at 10.26.04 copy.jpg>
> Larry

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

More information about the isabelle-dev mailing list