src/HOL/Divides.thy
changeset 37767 a2b7a20d6ea3
parent 36634 f9b43d197d16
child 38715 6513ea67d95d
     1.1 --- a/src/HOL/Divides.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -527,7 +527,7 @@
     1.4  begin
     1.5  
     1.6  definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
     1.7 -  [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
     1.8 +  "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
     1.9  
    1.10  lemma divmod_nat_rel_divmod_nat:
    1.11    "divmod_nat_rel m n (divmod_nat m n)"