Re: [isabelle-dev] code abbreviation for mapping over a fixed range

Hi Florian, > > This email refers to the following commit: > > > > http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251 > > > > code abbreviation for mapping over a fixed range > > > > Is there a specific reason for this code equation: > > > > "map_range f (Suc n) = map_range f n @

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

On Fri, 6 Nov 2015, Makarius wrote: On Wed, 4 Nov 2015, Clemens Ballarin wrote: On 30 October, 2015 20:02 CET, Makarius wrote: > Standard batch build prints relatively few terms, so this is not yet > significant as a test. > > The following change prints every