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 >
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
