[isabelle-dev] ZF/upair.thy failing

[Lawrence Paulson]

Also in ZF/Inductive_ZF.thy...
Larry

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>