# HG changeset patch
# User huffman
# Date 1333088129 -7200
# Node ID e1b0c8236ae42b5ace8e3f6eb6443bcf11a50cbf
# Parent  b1dd32b2a505fdf77fd15a4b0c51e18a5230f5d8
fix search-and-replace errors

diff -r b1dd32b2a505 -r e1b0c8236ae4 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Fri Mar 30 08:04:28 2012 +0200
+++ b/src/HOL/Num.thy	Fri Mar 30 08:15:29 2012 +0200
@@ -230,10 +230,10 @@
   by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
 
 
-subsection {* Numary numerals *}
+subsection {* Binary numerals *}
 
 text {*
-  We embed numary representations into a generic algebraic
+  We embed binary representations into a generic algebraic
   structure using @{text numeral}.
 *}
 
@@ -967,7 +967,7 @@
   "inverse Numeral1 = (Numeral1::'a::division_ring)"
   by simp
 
-text{*Theorem lists for the cancellation simprocs. The use of a numary
+text{*Theorem lists for the cancellation simprocs. The use of a binary
 numeral for 1 reduces the number of special cases.*}
 
 lemmas mult_1s =