# HG changeset patch
# User blanchet
# Date 1378993604 -7200
# Node ID 1e5314b990098ea9fa992bf17d241028aea52718
# Parent  778b2b8f4a352ec98ffbf6cb5ed8ce6fe0b78f0a
add a notice to myself in doc

diff -r 778b2b8f4a35 -r 1e5314b99009 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 12 15:14:54 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 12 15:46:44 2013 +0200
@@ -1334,6 +1334,8 @@
 * no way to register same type as both data- and codatatype?
 
 * no recursion through unused arguments (unlike with the old package)
+
+* in a locale, cannot use locally fixed types (because of limitation in typedef)?
 *}