Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
improved naming of complex theorems in presentation;
authorwenzelm
Tue, 31 May 2005 11:53:10 +0200
changeset 16119 c0916ed7b8e9
parent 16118 921936bd8847
child 16120 6a449deff8d9
improved naming of complex theorems in presentation; typedef: sorts *are* allowed, but only on the rhs;
TODO file | annotate | diff | comparison | revisions 
--- 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)
isabelle