src/HOL/ex/Numeral.thy

 (*  Title:      HOL/ex/Numeral.thy
-    ID:         $Id$
     Author:     Florian Haftmann
 
 An experimental alternative numeral representation.
 *)
 

 
 subsection {* Binary numerals *}
 
 text {*
   We embed binary representations into a generic algebraic
-  structure using @{text of_num}
+  structure using @{text of_num}.
 *}
 
 ML {*
 structure DigSimps =
   NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")

 hide (open) const sub dup
 
 
 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]
 declare (in ring_1) numeral [simp]
 thm numeral