We can be very proud of these figures. I have occasionally compared the source releases of Certain Other Systems over time, and noticed that proofs are still write-only: new proofs are added, but existing proofs are almost never changed.
Larry > On 28 Sep 2017, at 13:20, Tobias Nipkow <nip...@in.tum.de> wrote: > > The whole project started with this AFP paper: > > http://www21.in.tum.de/~nipkow/pubs/cicm15.html > <http://www21.in.tum.de/~nipkow/pubs/cicm15.html> > > First Max developed this just to support the statistics in the paper but then > he and Lars made it part of the AFP. There is also a hidden part that > generates tex files for these and a number of further statistics that I use > for talks. > > Concerning growth of articles. I am not sure we want to provide more > finegrained statistics for every entry, but attached you find a summary > slide. I cannot remember precisely what is measured, but at a first > approximation it tells us that over time every second line of an AFP entry is > modified. > > Tobias
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev