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

Currently heating my CPU with test-building the patch ... If everything goes fine, I will push it. -- Peter On Do, 2015-11-19 at 10:46 +0100, Florian Haftmann wrote: > Hi all, > > >> These suggestions are worth a discussion. Should we go ahead? Would > anybody like to apply this patch and

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

Hi all, >> These suggestions are worth a discussion. Should we go ahead? Would anybody like to apply this patch and test that everything still works? > > I could do it, if nobody has objections. I see no obstacles in going ahead. What requires some thought is the material in ex/ directories is

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

As I recall, the Library directory get special treatment. But I forget what this special treatment consists of. It might make sense to move this particular entry to Library. Larry > On 19 Nov 2015, at 09:46, Florian Haftmann > wrote: > > Hi all, >

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

> On 18.11.2015, at 16:26, 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? I could do it, if nobody has objections. Jasmin

[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

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

… and this time with the patch … > On 15 Nov 2015, at 22:15, Peter Gammie 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