[isabelle-dev] Someone messed up HOL_library/Multiset_Order
Peter Lammich
lammich at in.tum.de
Thu Mar 26 14:00:25 CET 2015
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 root.log.
*** Undefined fact: "comm_monoid_diff_class.diff_cancel" (line 302 of
"~~/src/HOL/Library/Multiset_Order.thy")
*** At command "by" (line 302 of
"~~/src/HOL/Library/Multiset_Order.thy")
More information about the isabelle-dev
mailing list