a first guess to avoid the Codegenerator_Test to loop infinitely
authorbulwahn
Thu, 12 Jul 2012 16:22:33 +0200
changeset 48253 4410a709913c
parent 48252 e98c3d50ae62
child 48254 63e0ca00b952
a first guess to avoid the Codegenerator_Test to loop infinitely
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Relation.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 21:46:11 2012 +1000
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 16:22:33 2012 +0200
@@ -138,10 +138,6 @@
   [code del]: "div_mod n m = (n div m, n mod m)"
 
 lemma [code]:
-  "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
-  unfolding div_mod_def by auto
-
-lemma [code]:
   "n div m = fst (div_mod n m)"
   unfolding div_mod_def by simp
 
--- a/src/HOL/Relation.thy	Thu Jul 12 21:46:11 2012 +1000
+++ b/src/HOL/Relation.thy	Thu Jul 12 16:22:33 2012 +0200
@@ -427,7 +427,7 @@
 
 definition Id :: "'a rel"
 where
-  "Id = {p. \<exists>x. p = (x, x)}"
+  [code del]: "Id = {p. \<exists>x. p = (x, x)}"
 
 lemma IdI [intro]: "(a, a) : Id"
   by (simp add: Id_def)