1.1 --- a/src/HOL/Word/BinBoolList.thy	Tue Jan 15 16:19:21 2008 +0100
     1.2 +++ b/src/HOL/Word/BinBoolList.thy	Tue Jan 15 16:19:23 2008 +0100
     1.3 @@ -76,13 +76,13 @@
     1.4    by (induct n) (auto simp: butlast_take)
     1.5  
     1.6  lemma bin_to_bl_aux_Pls_minus_simp:
     1.7 -  "0 < n ==> bin_to_bl_aux n Numeral.Pls bl = 
     1.8 -    bin_to_bl_aux (n - 1) Numeral.Pls (False # bl)"
     1.9 +  "0 < n ==> bin_to_bl_aux n Int.Pls bl = 
    1.10 +    bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
    1.11    by (cases n) auto
    1.12  
    1.13  lemma bin_to_bl_aux_Min_minus_simp:
    1.14 -  "0 < n ==> bin_to_bl_aux n Numeral.Min bl = 
    1.15 -    bin_to_bl_aux (n - 1) Numeral.Min (True # bl)"
    1.16 +  "0 < n ==> bin_to_bl_aux n Int.Min bl = 
    1.17 +    bin_to_bl_aux (n - 1) Int.Min (True # bl)"
    1.18    by (cases n) auto
    1.19  
    1.20  lemma bin_to_bl_aux_Bit_minus_simp:
    1.21 @@ -166,21 +166,21 @@
    1.22  lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
    1.23    unfolding bl_to_bin_def by auto
    1.24    
    1.25 -lemma bl_to_bin_Nil: "bl_to_bin [] = Numeral.Pls"
    1.26 +lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
    1.27    unfolding bl_to_bin_def by auto
    1.28  
    1.29  lemma bin_to_bl_Pls_aux [rule_format] : 
    1.30 -  "ALL bl. bin_to_bl_aux n Numeral.Pls bl = replicate n False @ bl"
    1.31 +  "ALL bl. bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
    1.32    by (induct n) (auto simp: replicate_app_Cons_same)
    1.33  
    1.34 -lemma bin_to_bl_Pls: "bin_to_bl n Numeral.Pls = replicate n False"
    1.35 +lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False"
    1.36    unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux)
    1.37  
    1.38  lemma bin_to_bl_Min_aux [rule_format] : 
    1.39 -  "ALL bl. bin_to_bl_aux n Numeral.Min bl = replicate n True @ bl"
    1.40 +  "ALL bl. bin_to_bl_aux n Int.Min bl = replicate n True @ bl"
    1.41    by (induct n) (auto simp: replicate_app_Cons_same)
    1.42  
    1.43 -lemma bin_to_bl_Min: "bin_to_bl n Numeral.Min = replicate n True"
    1.44 +lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True"
    1.45    unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux)
    1.46  
    1.47  lemma bl_to_bin_rep_F: 
    1.48 @@ -214,7 +214,7 @@
    1.49  lemmas bin_to_bl_bintr = 
    1.50    bin_to_bl_aux_bintr [where bl = "[]", folded bin_to_bl_def]
    1.51  
    1.52 -lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Numeral.Pls"
    1.53 +lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
    1.54    by (induct n) auto
    1.55  
    1.56  lemma len_bin_to_bl_aux [rule_format] : 
    1.57 @@ -228,12 +228,12 @@
    1.58    "ALL w. bin_sign (bl_to_bin_aux w bs) = bin_sign w"
    1.59    by (induct bs) auto
    1.60    
    1.61 -lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Numeral.Pls"
    1.62 +lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls"
    1.63    unfolding bl_to_bin_def by (simp add : sign_bl_bin')
    1.64    
    1.65  lemma bl_sbin_sign_aux [rule_format] : 
    1.66    "ALL w bs. hd (bin_to_bl_aux (Suc n) w bs) = 
    1.67 -    (bin_sign (sbintrunc n w) = Numeral.Min)"
    1.68 +    (bin_sign (sbintrunc n w) = Int.Min)"
    1.69    apply (induct "n")
    1.70     apply clarsimp
    1.71     apply (case_tac w rule: bin_exhaust)
    1.72 @@ -242,7 +242,7 @@
    1.73    done
    1.74      
    1.75  lemma bl_sbin_sign: 
    1.76 -  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Numeral.Min)"
    1.77 +  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
    1.78    unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
    1.79  
    1.80  lemma bin_nth_of_bl_aux [rule_format] : 
    1.81 @@ -658,7 +658,7 @@
    1.82    by (induct nw) auto 
    1.83  
    1.84  lemmas bl_to_bin_aux_alt = 
    1.85 -  bl_to_bin_aux_cat [where nv = "0" and v = "Numeral.Pls", 
    1.86 +  bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls", 
    1.87      simplified bl_to_bin_def [symmetric], simplified]
    1.88  
    1.89  lemmas bin_to_bl_cat =
    1.90 @@ -671,7 +671,7 @@
    1.91    trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
    1.92  
    1.93  lemmas bl_to_bin_app_cat = bl_to_bin_aux_app_cat
    1.94 -  [where w = "Numeral.Pls", folded bl_to_bin_def]
    1.95 +  [where w = "Int.Pls", folded bl_to_bin_def]
    1.96  
    1.97  lemmas bin_to_bl_cat_app = bin_to_bl_aux_cat_app
    1.98    [where bs = "[]", folded bin_to_bl_def]
    1.99 @@ -682,7 +682,7 @@
   1.100    by (simp add : bl_to_bin_app_cat)
   1.101  
   1.102  lemma mask_lem: "(bl_to_bin (True # replicate n False)) = 
   1.103 -    Numeral.succ (bl_to_bin (replicate n True))"
   1.104 +    Int.succ (bl_to_bin (replicate n True))"
   1.105    apply (unfold bl_to_bin_def)
   1.106    apply (induct n)
   1.107     apply simp
   1.108 @@ -745,7 +745,7 @@
   1.109    rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
   1.110  
   1.111  lemma rbl_pred: 
   1.112 -  "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Numeral.pred bin))"
   1.113 +  "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.pred bin))"
   1.114    apply (induct n, simp)
   1.115    apply (unfold bin_to_bl_def)
   1.116    apply clarsimp
   1.117 @@ -755,7 +755,7 @@
   1.118    done
   1.119  
   1.120  lemma rbl_succ: 
   1.121 -  "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Numeral.succ bin))"
   1.122 +  "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.succ bin))"
   1.123    apply (induct n, simp)
   1.124    apply (unfold bin_to_bl_def)
   1.125    apply clarsimp
   1.126 @@ -1011,7 +1011,7 @@
   1.127  lemma bin_split_pred_simp [simp]: 
   1.128    "(0::nat) < number_of bin \<Longrightarrow>
   1.129    bin_split (number_of bin) w =
   1.130 -  (let (w1, w2) = bin_split (number_of (Numeral.pred bin)) (bin_rest w)
   1.131 +  (let (w1, w2) = bin_split (number_of (Int.pred bin)) (bin_rest w)
   1.132     in (w1, w2 BIT bin_last w))" 
   1.133    by (simp only: nobm1 bin_split_minus_simp)
   1.134