[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