src/HOL/Parity.thy
changeset 58709 efdc6c533bd3
parent 58691 68f8d22a6867
child 58710 7216a10d69ba
     1.1 --- a/src/HOL/Parity.thy	Sun Oct 19 12:47:34 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Sun Oct 19 18:05:26 2014 +0200
     1.3 @@ -514,14 +514,6 @@
     1.4  
     1.5  subsubsection {* Miscellaneous *}
     1.6  
     1.7 -lemma even_mult_two_ex:
     1.8 -  "even(n) = (\<exists>m::nat. n = 2*m)"
     1.9 -  by presburger
    1.10 -
    1.11 -lemma odd_Suc_mult_two_ex:
    1.12 -  "odd(n) = (\<exists>m. n = Suc (2*m))"
    1.13 -  by presburger
    1.14 -
    1.15  lemma even_nat_plus_one_div_two:
    1.16    "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
    1.17    by presburger