# HG changeset patch
# User haftmann
# Date 1205347093 -3600
# Node ID 89e25cc8da7a7bb4811966501cbccfe843a12292
# Parent  c95b91870e3b76b38c993dd23fbec206933fa791
yet another useful lemma

diff -r c95b91870e3b -r 89e25cc8da7a src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Wed Mar 12 17:29:09 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Wed Mar 12 19:38:13 2008 +0100
@@ -139,6 +139,10 @@
 
 end
 
+lemma nat_of_index_number [simp]:
+  "nat_of_index (number_of k) = number_of k"
+  by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
+
 code_datatype "number_of \<Colon> int \<Rightarrow> index"