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/Divides.thy
changeset 37767 a2b7a20d6ea3
parent 36634 f9b43d197d16
child 38715 6513ea67d95d 
--- a/src/HOL/Divides.thy	Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Divides.thy	Mon Jul 12 10:48:37 2010 +0200
@@ -527,7 +527,7 @@
 begin
 
 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
-  [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
+  "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
 
 lemma divmod_nat_rel_divmod_nat:
   "divmod_nat_rel m n (divmod_nat m n)"
isabelle