1.1 --- a/src/HOL/Int.thy	Thu Dec 04 11:14:24 2008 -0800
     1.2 +++ b/src/HOL/Int.thy	Thu Dec 04 12:32:38 2008 -0800
     1.3 @@ -855,7 +855,7 @@
     1.4      add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
     1.5  qed
     1.6  
     1.7 -lemma neg_simps:
     1.8 +lemma bin_less_0_simps:
     1.9    "Pls < 0 \<longleftrightarrow> False"
    1.10    "Min < 0 \<longleftrightarrow> True"
    1.11    "Bit0 w < 0 \<longleftrightarrow> w < 0"
    1.12 @@ -908,7 +908,7 @@
    1.13      less_bin_lemma [of "Bit1 k"]
    1.14      less_bin_lemma [of "pred Pls"]
    1.15      less_bin_lemma [of "pred k"]
    1.16 -  by (simp_all add: neg_simps succ_pred)
    1.17 +  by (simp_all add: bin_less_0_simps succ_pred)
    1.18  
    1.19  text {* Less-than-or-equal *}
    1.20  
    1.21 @@ -1187,6 +1187,12 @@
    1.22      by (auto simp add: iszero_def number_of_eq numeral_simps)
    1.23  qed
    1.24  
    1.25 +lemmas iszero_simps =
    1.26 +  iszero_0 not_iszero_1
    1.27 +  iszero_number_of_Pls nonzero_number_of_Min
    1.28 +  iszero_number_of_Bit0 iszero_number_of_Bit1
    1.29 +(* iszero_number_of_Pls would never normally be used
    1.30 +   because its lhs simplifies to "iszero 0" *)
    1.31  
    1.32  subsubsection {* The Less-Than Relation *}
    1.33  
    1.34 @@ -1248,6 +1254,10 @@
    1.35    by (simp add: neg_def number_of_eq numeral_simps)
    1.36  qed
    1.37  
    1.38 +lemmas neg_simps =
    1.39 +  not_neg_0 not_neg_1
    1.40 +  not_neg_number_of_Pls neg_number_of_Min
    1.41 +  neg_number_of_Bit0 neg_number_of_Bit1
    1.42  
    1.43  text {* Less-Than or Equals *}
    1.44  
    1.45 @@ -1315,12 +1325,7 @@
    1.46    less_number_of less_bin_simps
    1.47    le_number_of le_bin_simps
    1.48    eq_number_of eq_bin_simps
    1.49 -  iszero_0 nonzero_number_of_Min
    1.50 -  iszero_number_of_Bit0 iszero_number_of_Bit1
    1.51 -  not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
    1.52 -  neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
    1.53 -(* iszero_number_of_Pls would never be used
    1.54 -   because its lhs simplifies to "iszero 0" *)
    1.55 +  iszero_simps neg_simps
    1.56  
    1.57  
    1.58  subsubsection {* Simplification of arithmetic when nested to the right. *}