# HG changeset patch
# User wenzelm
# Date 1117533190 -7200
# Node ID c0916ed7b8e9c2b763d65904f07acc26b1eadafe
# Parent  921936bd88476c36c0be5bf251e6f49682296a92
improved naming of complex theorems in presentation;
typedef: sorts *are* allowed, but only on the rhs;

diff -r 921936bd8847 -r c0916ed7b8e9 TODO
--- a/TODO	Tue May 31 11:00:59 2005 +0200
+++ b/TODO	Tue May 31 11:53:10 2005 +0200
@@ -25,11 +25,4 @@
 
 - ball, bex and setsum congruence rules (Tobias & Stefan)
 
-- html generation: somtimes lemma names and whole lemmas are missing.
-  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)