On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann <span dir="ltr"><<a href="mailto:florian.haftmann@informatik.tu-muenchen.de">florian.haftmann@informatik.tu-muenchen.de</a>></span> wrote:<br><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">[...] So, the best way now is<br>
to continue eliminating set-pred mixture (also in the AFP of course!)<br>
and discover problems in packages – I'm a little concerned about<br>
quotient since this has been introduced after 2008, but maybe Cezary can<br>
comment on this.</blockquote><div><br></div><div>Hi Florian,</div><div><br></div><div><div>I already made the changes to the core of the quotient package as of:</div><div><a href="http://isabelle.in.tum.de/repos/isabelle/rev/3cdc4176638c">http://isabelle.in.tum.de/repos/isabelle/rev/3cdc4176638c</a></div>
<div><br></div><div>With the above the quotient package works both as is and with the</div><div>explicit set type.</div><div><br></div><div>It seems you included only a part of the above changeset in the</div><div>isabelle_set repository, in particular the change in the</div>
<div>src/HOL/Equiv_Relations.thy is necessary but seems it did not go in.</div><div>With this change the quotient package works and only changes to the</div><div>particular examples may be needed, but many work without any changes:</div>
<div><br></div><div>New Nominal: Works.</div><div><br></div><div>Quotient_Message: Works.</div><div>Quotient_Int: Works.</div><div>FSet: Requires removing one 'simp add: mem_def', then works.</div><div>DList: I pushed a change 5 min ago; with it it works.</div>
<div><br></div><div>CSet and List_Cset depend on Library/More_Set which doesn't load, so</div><div>I can't say if there are any quotient issues...</div><div><br></div><div>AFP/Coinductive needs updating, long before quotients it does:</div>
<div>  enat_set :: "enat => bool" so I can't say without going further in the</div><div>  code.</div><div><br></div><div>Regards,</div><div><br></div><div>Cezary.</div></div><div><br></div></div>