# HG changeset patch
# User nipkow
# Date 1114446580 -7200
# Node ID 2aee4e5b792509a2742ce6a25941edf75452f456
# Parent  7a567dcd4cda394e6a98e4645058186ab7ce2c0e
*** empty log message ***

diff -r 7a567dcd4cda -r 2aee4e5b7925 TODO
--- a/TODO	Mon Apr 25 17:58:41 2005 +0200
+++ b/TODO	Mon Apr 25 18:29:40 2005 +0200
@@ -33,4 +33,7 @@
   See http://afp.sourceforge.net/browser_info/current/HOL/HOL-Complex/Integration/SetsumThms.html
   (Markus?)
 
+- Allow sorts in typedef:  typedef ('a::mysort)t = ...
+  (low priority)
+
 - remove this file (Tobias)