Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Int.thy
changeset 30000 453077188eac
parent 29955 61837a9bdd74
child 30079 293b896b9c25 
--- 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