remove unnecessary qualifiers on names
authorhuffman
Mon Apr 02 16:07:24 2012 +0200 (2012-04-02)
changeset 473002284a40e0f57
parent 47299 e705ef5ffe95
child 47301 ca743eafa1dd
remove unnecessary qualifiers on names
src/HOL/Num.thy
     1.1 --- a/src/HOL/Num.thy	Mon Apr 02 16:06:24 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Mon Apr 02 16:07:24 2012 +0200
     1.3 @@ -193,7 +193,7 @@
     1.4  text {* The @{const num_of_nat} conversion *}
     1.5  
     1.6  lemma num_of_nat_One:
     1.7 -  "n \<le> 1 \<Longrightarrow> num_of_nat n = Num.One"
     1.8 +  "n \<le> 1 \<Longrightarrow> num_of_nat n = One"
     1.9    by (cases n) simp_all
    1.10  
    1.11  lemma num_of_nat_plus_distrib:
    1.12 @@ -884,9 +884,9 @@
    1.13    by (simp_all add: numeral.simps BitM_plus_one)
    1.14  
    1.15  lemma pred_numeral_simps [simp]:
    1.16 -  "pred_numeral Num.One = 0"
    1.17 -  "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
    1.18 -  "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
    1.19 +  "pred_numeral One = 0"
    1.20 +  "pred_numeral (Bit0 k) = numeral (BitM k)"
    1.21 +  "pred_numeral (Bit1 k) = numeral (Bit0 k)"
    1.22    unfolding pred_numeral_def eval_nat_numeral
    1.23    by (simp_all only: diff_Suc_Suc diff_0)
    1.24  
    1.25 @@ -900,7 +900,7 @@
    1.26    by (simp only: numeral_One One_nat_def)
    1.27  
    1.28  lemma Suc_nat_number_of_add:
    1.29 -  "Suc (numeral v + n) = numeral (v + Num.One) + n"
    1.30 +  "Suc (numeral v + n) = numeral (v + One) + n"
    1.31    by simp
    1.32  
    1.33  (*Maps #n to n for n = 1, 2*)