src/HOL/Word/WordDefinition.thy

   "word_power == op ^"
 
 definition
   word_succ :: "'a :: len0 word => 'a word"
 where
-  "word_succ a = word_of_int (Numeral.succ (uint a))"
+  "word_succ a = word_of_int (Int.succ (uint a))"
 
 definition
   word_pred :: "'a :: len0 word => 'a word"
 where
-  "word_pred a = word_of_int (Numeral.pred (uint a))"
+  "word_pred a = word_of_int (Int.pred (uint a))"
 
 constdefs
   udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
   "a udvd b == EX n>=0. uint b = n * uint a"
 

 
   word_lsb_def: 
   "lsb (a::'a::len0 word) == bin_last (uint a) = bit.B1"
 
   word_msb_def: 
-  "msb (a::'a::len word) == bin_sign (sint a) = Numeral.Min"
+  "msb (a::'a::len word) == bin_sign (sint a) = Int.Min"
 
 
 constdefs
   setBit :: "'a :: len0 word => nat => 'a word" 
   "setBit w n == set_bit w n True"

 lemmas uint_lt2p [iff] = uint_lem [THEN conjunct2, standard]
 lemmas sint_ge = sint_lem [THEN conjunct1, standard]
 lemmas sint_lt = sint_lem [THEN conjunct2, standard]
 
 lemma sign_uint_Pls [simp]: 
-  "bin_sign (uint x) = Numeral.Pls"
+  "bin_sign (uint x) = Int.Pls"
   by (simp add: sign_Pls_ge_0 number_of_eq)
 
 lemmas uint_m2p_neg = iffD2 [OF diff_less_0_iff_less uint_lt2p, standard]
 lemmas uint_m2p_not_non_neg = 
   iffD2 [OF linorder_not_le uint_m2p_neg, standard]

   "uint (number_of b :: 'a :: len0 word) = number_of b mod 2 ^ len_of TYPE('a)"
   unfolding word_number_of_alt
   by (simp only: int_word_uint)
 
 lemma unat_number_of: 
-  "bin_sign b = Numeral.Pls ==> 
+  "bin_sign b = Int.Pls ==> 
   unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
   apply (unfold unat_def)
   apply (clarsimp simp only: uint_number_of)
   apply (rule nat_mod_distrib [THEN trans])
     apply (erule sign_Pls_ge_0 [THEN iffD1])

 lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' len_gt_0, standard]
 lemmas bl_not_Nil [iff] = 
   length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
 lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
 
-lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Numeral.Min)"
+lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Int.Min)"
   apply (unfold to_bl_def sint_uint)
   apply (rule trans [OF _ bl_sbin_sign])
   apply simp
   done