# HG changeset patch # User wenzelm # Date 1344514176 -7200 # Node ID 28d59ce5ebfd950286f42e80618e291f756ef4d7 # Parent 98e98181882d5cc935fc60211557a80d0269a585 explicit FIXME; diff -r 98e98181882d -r 28d59ce5ebfd src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Thu Aug 09 12:39:05 2012 +0200 +++ b/src/HOL/Library/Library.thy Thu Aug 09 14:09:36 2012 +0200 @@ -55,7 +55,7 @@ Ramsey Reflection RBT_Mapping - (* RBT_Set *) (* not included because it breaks Codegenerator_Test/Generate*.thy *) + (* RBT_Set *) (* FIXME not included because it breaks Codegenerator_Test/Generate*.thy *) Saturated Set_Algebras State_Monad