On Sun, 5 Sep 2010, Tjark Weber wrote:
On Fri, 2010-09-03 at 15:06 +0200, Makarius wrote:
When composing log messages it is important do this from the perspective
of someone who needs to figure out problems many months/years later, and
needs to understand what was truely happening at some
Does it mean it's from that changeset?
changeset: 39036:dff91b90d74c
user:blanchet
date:Thu Sep 02 11:29:02 2010 +0200
files: src/HOL/HOL.thy src/HOL/Hilbert_Choice.thy src/HOL/SAT.thy
src/HOL/Sledgehammer.thy src/HOL/Tools/Sledgehammer/clausifier.ML
description:
On Sat, 4 Sep 2010, Jasmin Christian Blanchette wrote:
When composing log messages it is important do this from the
perspective of someone who needs to figure out problems many
months/years later, and needs to understand what was truely happening
at some point.
And public mailing lists are
On Fri, 2010-09-03 at 15:06 +0200, Makarius wrote:
When composing log messages it is important do this from the perspective
of someone who needs to figure out problems many months/years later, and
needs to understand what was truely happening at some point.
tuned
Regards,
Tjark
Today's isatest indicates a significant drop in performance:
http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png
http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png
http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png
Makarius
Am 03.09.2010 um 13:37 schrieb Makarius:
Today's isatest indicates a significant drop in performance:
http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png
http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png
