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.
deleted looping code theorem
authorhaftmann
Wed, 28 Nov 2007 15:09:19 +0100
changeset 25488 c945521fa0d9
parent 25487 d96d5808d926
child 25489 5b0625f6e324
deleted looping code theorem
src/HOL/Library/Efficient_Nat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Nov 28 14:56:38 2007 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Nov 28 15:09:19 2007 +0100
@@ -33,7 +33,7 @@
 
 definition
   int_of_nat :: "nat \<Rightarrow> int" where
-  "int_of_nat n = of_nat n"
+  [code func del]: "int_of_nat n = of_nat n"
 
 lemma int_of_nat_Suc [simp]:
   "int_of_nat (Suc n) = 1 + int_of_nat n"
isabelle