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.
nat_number_of is no longer declared as code lemma, since this turned
authorberghofe
Tue, 27 Sep 2005 12:16:06 +0200
changeset 17668 8ef257366a0c
parent 17667 2beb71c0f92e
child 17669 94dbbffbf94b
nat_number_of is no longer declared as code lemma, since this turned out to be too inefficient.
src/HOL/Integ/NatBin.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/NatBin.thy	Tue Sep 27 12:14:39 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue Sep 27 12:16:06 2005 +0200
@@ -28,8 +28,6 @@
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
 by (simp add: nat_number_of_def)
 
-declare nat_number_of [symmetric, THEN eq_reflection, code unfold]
-
 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
 by (simp add: nat_number_of_def)
isabelle