[isabelle-dev] HOL-Predicate_Compile_Examples

Makarius makarius at sketis.net
Wed Sep 9 22:03:27 CEST 2015

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.


More information about the isabelle-dev mailing list