# HG changeset patch
# User huffman
# Date 1179766384 -7200
# Node ID 68b152e8ea86be69b2b1d5cc7b2a3dfe40a7f463
# Parent  448827ccd9e9adafe6ec81f341b5cd426275d24a
add lemmas divide_numeral_1 and inverse_numeral_1

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.*}