Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
declare of_int_number_of_eq [simp]
authorhuffman
Thu, 19 Feb 2009 18:16:19 -0800
changeset 30000 453077188eac
parent 29999 da85a244e328
child 30001 dd27e16677b2
declare of_int_number_of_eq [simp]
src/HOL/Int.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle