diff --git a/TODO.txt b/TODO.txt
index 48e3de9d13186fabbc738f118a95d1499bc354f6..52628e51b3dc879a2151648ec9db33c6061ebd08 100644
--- a/TODO.txt
+++ b/TODO.txt
@@ -1,8 +1,3 @@
-Change retag semantics! Don't prove anything about this crazy monster.
-
-Things in the "logical" side of the model that could be made better:
-- Free and Retag should be WF!
-
 More speculative:
 - Can the separate private/local things be better integrated to the notion of a "private location" for the purposes of stating lemmas about them?
   Basically, can "protected" become another state of the tag? How can we make sure a call ID protects nothing when EndCall happens?