--- a/src/HOL/Integ/IntArith.thy Mon May 21 16:39:58 2007 +0200
+++ b/src/HOL/Integ/IntArith.thy Mon May 21 18:53:04 2007 +0200
@@ -28,6 +28,13 @@
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
by simp
+lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
+by simp
+
+lemma inverse_numeral_1:
+ "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
+by simp
+
text{*Theorem lists for the cancellation simprocs. The use of binary numerals
for 0 and 1 reduces the number of special cases.*}