remove hidden fact about hidden constant from code generator setup
authorblanchet
Wed Feb 12 08:37:28 2014 +0100 (2014-02-12)
changeset 554249ab4129a76a3
parent 55423 07dea66779f3
child 55425 7a3e78ee813b
remove hidden fact about hidden constant from code generator setup
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
     1.3 @@ -119,6 +119,8 @@
     1.4  abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
     1.5    "rec_nat \<equiv> old.rec_nat"
     1.6  
     1.7 +declare nat.sel[code del]
     1.8 +
     1.9  hide_const Nat.pred -- {* hide everything related to the selector *}
    1.10  hide_fact
    1.11    nat.case_eq_if
    1.12 @@ -1943,13 +1945,13 @@
    1.13  qed
    1.14  
    1.15  
    1.16 -subsection {* aliasses *}
    1.17 +subsection {* aliases *}
    1.18  
    1.19  lemma nat_mult_1: "(1::nat) * n = n"
    1.20 -  by simp
    1.21 +  by (rule mult_1_left)
    1.22   
    1.23  lemma nat_mult_1_right: "n * (1::nat) = n"
    1.24 -  by simp
    1.25 +  by (rule mult_1_right)
    1.26  
    1.27  
    1.28  subsection {* size of a datatype value *}