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

[Peter Gammie]

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