# HG changeset patch
# User huffman
# Date 1235096179 28800
# Node ID 453077188eac302c5a0649e6ef9e5bbf58df4fc3
# Parent  da85a244e328a5dcbd1c3107a4bdd1990ea47d9b
declare of_int_number_of_eq [simp]

diff -r da85a244e328 -r 453077188eac src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Feb 19 17:13:35 2009 -0800
+++ b/src/HOL/Int.thy	Thu Feb 19 18:16:19 2009 -0800
@@ -1547,7 +1547,7 @@
      "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
 by (simp add: power_abs)
 
-lemma of_int_number_of_eq:
+lemma of_int_number_of_eq [simp]:
      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
 by (simp add: number_of_eq)