Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.
On Wed, 11 Dec 2013, David Greenaway wrote:
Do you really have 400k lines of Isabelle proof scripts? All of the
Isabelle/HOL theories (including examples and libraries) are barely
more than that.
~/l4.verified # rm -rf isabelle
~/l4.verified # wc -l **/*.thy | tail -1
Here is some raw information about afp-2013-2:
$ wc -c $(find afp-2013-2 -name "*.thy") | tail -1
$ wc -l $(find afp-2013-2 -name "*.thy") | tail -1
So the public material seems to outweigh the top-secret stuff.
This archive was generated by a fusion of
Pipermail (Mailman edition) and