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 "~~/src/HOL/Library/Multiset_Order.thy") >> Unfinished session(s): HOL-Library >> Finished at Thu Mar 26 01:54:14 CET 2015 >> 0:09:32 elapsed time, 0:19:54 cpu time, factor 2.08 >> >> I think Florian has been tuning this recently. > > Yes, he (cc:d) pushed changes after mine and thereby broke the build. (His > changes are older but he pushed them afterwards.) > > Jasmin >
-- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
