Hi again,
Am 17.09.2014 um 11:40 schrieb Jasmin Christian Blanchette
jasmin.blanche...@gmail.com:
1. HOL-Proofs times out since September 14 on at-poly-e. On September 13,
we had
Timing HOL-Proofs (2 threads, 3161.882s elapsed time, 2889.329s cpu time,
840.167s GC time, factor 0.91)
Dear developers,
Jasmin mentioned to me that his new implementation allows to select which plugins should
be applied. Currently, the code generator has its own manager of plugins
(Code.datatype_interpretation) and I would be very happy if certain plugins could be
disabled selectively upon
On 18/09/2014 15:47, Florian Haftmann wrote:
Changeset #fe083c681ed8 introduces products over lists. There has been
some private discussion whether there could be a serious attempt to
establish a new consistent naming scheme for summation and products over
collections.
a) for lists:
A gain in legibility for sure.
Larry
On 18 Sep 2014, at 15:11, Tobias Nipkow nip...@in.tum.de wrote:
On 18/09/2014 15:47, Florian Haftmann wrote:
Changeset #fe083c681ed8 introduces products over lists. There has been
some private discussion whether there could be a serious attempt to
When printing integers, there is a funny historic artefact:
Library.string_of_int :: int - string
examples 1705, ~42 -- ie. ML syntax
Library.signed_string_of_int :: int - string
examples 1705, -42 -- ie. conventional syntax
ML_Syntax.print_int is an
