--- a/src/HOL/ex/Numeral.thy Mon Feb 16 13:38:09 2009 +0100
+++ b/src/HOL/ex/Numeral.thy Mon Feb 16 13:38:10 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Numeral.thy
- ID: $Id$
Author: Florian Haftmann
An experimental alternative numeral representation.
@@ -249,7 +248,7 @@
text {*
We embed binary representations into a generic algebraic
- structure using @{text of_num}
+ structure using @{text of_num}.
*}
ML {*
@@ -891,7 +890,7 @@
subsection {* Numeral equations as default simplification rules *}
-text {* TODO. Be more precise here with respect to subsumed facts. *}
+text {* TODO. Be more precise here with respect to subsumed facts. Or use named theorems anyway. *}
declare (in semiring_numeral) numeral [simp]
declare (in semiring_1) numeral [simp]
declare (in semiring_char_0) numeral [simp]