On Mi, 2015-11-18 at 15:26 +0000, Lawrence Paulson wrote: > These suggestions are worth a discussion. Should we go ahead? Would anybody > like to apply this patch and test that everything still works?
Pushed. See Isabelle-dev, changeset 2e89bc578935 -- Peter > > Larry > > > Begin forwarded message: > > > > From: Peter Gammie <pete...@gmail.com> > > Date: 15 November 2015 at 15:15:48 GMT > > To: isabelle-dev@mailbroy.informatik.tu-muenchen.de > > Subject: [isabelle-dev] minor generalisation to > > Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to > > List_Sublist > > > > Hi, > > > > Can someone please apply the attached patch to Isabelle for me? > > > > It does three things: > > - generalises Imperative_Quicksort to work on linearly-ordered, > > heap-representable types, and not just nat > > - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist > > - mildly weakens the assumptions of lemma subarray_append in theory Subarray > > > > The first may require existing theories to add type annotations. If this is > > a concern then perhaps the right thing to do is introduce new names for the > > polymorphic operations and preserve the existing ones, but I think that is > > overkill. > > > > The second may also break existing theories but I do not know how to > > otherwise get around having two theories with the same name. > > > > thanks, > > peter > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
