--- 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)