… and this time with the patch … > On 15 Nov 2015, at 22:15, Peter Gammie <pete...@gmail.com> wrote: > > 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
Imperative_HOL.patch
Description: Binary data
-- http://peteg.org/
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
