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
