On Wed, 9 Sep 2015, Andreas Lochbihler wrote:
I've committed some changes in 78ece168f5b5 such that most of the examples work again. Only Hotel_Example_Small_Generator remains completely broken.
Great -- this is a clear move forward, and only one obscure FIXME remaining in src/HOL/ROOT.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
