
diff -r 448827ccd9e9 -r 68b152e8ea86 src/HOL/Integ/IntArith.thy
--- 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.*}
 




