[isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

2016-07-11 Thread Makarius
*** Prover IDE -- Isabelle/Scala/jEdit *** * Indentation according to Isabelle outer syntax, cf. action "indent-lines" (shortcut C+i). This refers to Isabelle/52349e41d5dc. It is only the second round of refinement, beyond direct imitation of the old proof-indent.el from Proof General (see

Re: [isabelle-dev] {0::nat..<n} = {..<n}

2016-07-11 Thread Florian Haftmann
> The whole setup has grown over time and initially I may have preferred > {..

Re: [isabelle-dev] Considered harmful: surj

2016-07-11 Thread Florian Haftmann
> Yes I second that. It surely is a good idea to just use it only as a > input translation. See now 6af79184bef3. Florian > > - Johannes > > Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann: >> Hi all, >> >> since cf26dd7395e4, ‹surj f› is a mere abbreviation

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Lars Hupel
>> I’m sure there are quite some papers which reference the /devel >> entries. > > I should hope not - they make no sense to cite, because their whole > purpose is to change on a daily basis. I'm with Gerwin here. In fact, the devel pages clearly state: "Please refer to release versions only in

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Andreas Lochbihler
For published versions, there probably should not be any /devel-entries links. But for papers under submission, people may have updated their AFP entries and want the reviewers to access the updated material. At least that is what I used to do for many ITP submissions. So it might be good to

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Gerwin Klein
On 11 Jul 2016, at 16:03, Johannes Hölzl wrote: > > Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel: >> Dear AFP developers, >> >> some of you may have noticed that the "AFP devel" pages have not been >> updated since April. This is partly my fault because I migrated

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Johannes Hölzl
Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel: > Dear AFP developers, > > some of you may have noticed that the "AFP devel" pages have not been > updated since April. This is partly my fault because I migrated the > infrastructure and partly not my fault because the scripts to