a first guess to avoid the Codegenerator_Test to loop infinitely
authorbulwahn
Thu Jul 12 16:22:33 2012 +0200 (2012-07-12)
changeset 482534410a709913c
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
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 21:46:11 2012 +1000
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 16:22:33 2012 +0200
     1.3 @@ -138,10 +138,6 @@
     1.4    [code del]: "div_mod n m = (n div m, n mod m)"
     1.5  
     1.6  lemma [code]:
     1.7 -  "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
     1.8 -  unfolding div_mod_def by auto
     1.9 -
    1.10 -lemma [code]:
    1.11    "n div m = fst (div_mod n m)"
    1.12    unfolding div_mod_def by simp
    1.13  
     2.1 --- a/src/HOL/Relation.thy	Thu Jul 12 21:46:11 2012 +1000
     2.2 +++ b/src/HOL/Relation.thy	Thu Jul 12 16:22:33 2012 +0200
     2.3 @@ -427,7 +427,7 @@
     2.4  
     2.5  definition Id :: "'a rel"
     2.6  where
     2.7 -  "Id = {p. \<exists>x. p = (x, x)}"
     2.8 +  [code del]: "Id = {p. \<exists>x. p = (x, x)}"
     2.9  
    2.10  lemma IdI [intro]: "(a, a) : Id"
    2.11    by (simp add: Id_def)