[isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Gammie]

… and this time with the patch …

> On 15 Nov 2015, at 22:15, Peter Gammie <peteg42 at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Imperative_HOL.patch
Type: application/octet-stream
Size: 6695 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151115/88fce386/attachment-0002.obj>
-------------- next part --------------

-- 
http://peteg.org/