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

[Peter Lammich]

On Mi, 2015-11-18 at 15: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?

Pushed. See Isabelle-dev, changeset 2e89bc578935

--
  Peter

> 
> Larry
> 
> > Begin forwarded message:
> > 
> > From: Peter Gammie 
> > Date: 15 November 2015 at 15:15:48 GMT
> > To: isabelle-dev@mailbroy.informatik.tu-muenchen.de
> > Subject: [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 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


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lawrence Paulson]

These suggestions are worth a discussion. Should we go ahead? Would anybody 
like to apply this patch and test that everything still works?

Larry

> Begin forwarded message:
> 
> From: Peter Gammie 
> Date: 15 November 2015 at 15:15:48 GMT
> To: isabelle-dev@mailbroy.informatik.tu-muenchen.de
> Subject: [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 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