OK, currently under analysis.
Am 26.03.2015 um 11:41 schrieb Jasmin Blanchette:
On 26.03.2015, at 11:34, Tobias Nipkow nip...@in.tum.de wrote:
*** Undefined fact: comm_monoid_diff_class.diff_cancel (line 302 of
~~/src/HOL/Library/Multiset_Order.thy)
*** At command by (line 302 of
http://isabelle.in.tum.de/reports/Isabelle/rev/75433c3ee203
Am 26.03.2015 um 11:42 schrieb Florian Haftmann:
OK, currently under analysis.
Am 26.03.2015 um 11:41 schrieb Jasmin Blanchette:
On 26.03.2015, at 11:34, Tobias Nipkow nip...@in.tum.de wrote:
*** Undefined fact:
Isabelle version: devel -- hg id 034b13f4efae
Test ended on: macbroy2, Thu Mar 26 13:46:35 CET 2015.
HOL-Library FAILED
(see
also
/home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.2_x86-darwin/log/HOL-Library)
Output written on root.pdf (710 pages, 1552625 bytes).
Transcript written on
On 26.03.2015, at 14:00, Peter Lammich lamm...@in.tum.de wrote:
Isabelle version: devel -- hg id 034b13f4efae
Someone pushed a fix a few hours ago already (75433c3ee203).
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de