src/HOL/ex/Binary.thy

          [@{simproc binary_nat_less_eq},
           @{simproc binary_nat_less},
           @{simproc binary_nat_diff},
           @{simproc binary_nat_div},
           @{simproc binary_nat_mod}]))))
-*} "binary simplification"
+*}
 
 
 subsection {* Concrete syntax *}
 
 syntax