# HG changeset patch
# User huffman
# Date 1205766785 -3600
# Node ID 988a103afbab8f6ec8077b4021a63bfd9d644fd2
# Parent  afc43168ed8586f940203d8ca08dda500c4e7015
remove unneeded constant mod_alt

diff -r afc43168ed85 -r 988a103afbab src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Mon Mar 17 11:42:46 2008 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy	Mon Mar 17 16:13:05 2008 +0100
@@ -47,9 +47,6 @@
 lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto
 
 constdefs
-  mod_alt :: "'a => 'a => 'a :: Divides.div"
-  "mod_alt n m == n mod m" 
-
   -- "alternative way of defining @{text bin_last}, @{text bin_rest}"
   bin_rl :: "int => int * bit" 
   "bin_rl w == SOME (r, l). w = r BIT l"
@@ -108,8 +105,7 @@
 
 -- "the inverse(s) of @{text number_of}"
 lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
-  using pos_mod_sign2 [of n] pos_mod_bound2 [of n]
-  unfolding mod_alt_def [symmetric] by auto
+  by (cases "n mod 2 = 0", simp_all)
 
 lemma emep1:
   "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"