Re: [isabelle-dev] Multiset_Order

2015-03-26 Thread 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: comm_monoid_diff_class.diff_cancel (line 302 of ~~/src/HOL/Library/Multiset_Order.thy) *** At command by (line 302 of

Re: [isabelle-dev] Multiset_Order

2015-03-26 Thread Florian Haftmann
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-dev] Someone messed up HOL_library/Multiset_Order

2015-03-26 Thread Peter Lammich
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

Re: [isabelle-dev] Someone messed up HOL_library/Multiset_Order

2015-03-26 Thread Jasmin Blanchette
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