# HG changeset patch
# User haftmann
# Date 1234787890 -3600
# Node ID 5d81dd706206aa8f3e16f18ea5e2a99c7d27f954
# Parent  125d513d9e39aa4a9fe04c70a6130ed6f86f7c5b
tuned texts

diff -r 125d513d9e39 -r 5d81dd706206 src/HOL/ex/Numeral.thy
--- 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]