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
 536136 total

Here is some raw information about afp-2013-2:

$ wc -c $(find afp-2013-2 -name "*.thy") | tail -1
39685684 total

$ wc -l $(find afp-2013-2 -name "*.thy") | tail -1
885191 total

So the public material seems to outweigh the top-secret stuff.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.