# HG changeset patch
# User blanchet
# Date 1392190648 -3600
# Node ID 9ab4129a76a3ae7b565d93dc96323af4bacb1a15
# Parent  07dea66779f33be28eef59c7a3bcfc08eefe49de
remove hidden fact about hidden constant from code generator setup

diff -r 07dea66779f3 -r 9ab4129a76a3 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
@@ -119,6 +119,8 @@
 abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
   "rec_nat \<equiv> old.rec_nat"
 
+declare nat.sel[code del]
+
 hide_const Nat.pred -- {* hide everything related to the selector *}
 hide_fact
   nat.case_eq_if
@@ -1943,13 +1945,13 @@
 qed
 
 
-subsection {* aliasses *}
+subsection {* aliases *}
 
 lemma nat_mult_1: "(1::nat) * n = n"
-  by simp
+  by (rule mult_1_left)
  
 lemma nat_mult_1_right: "n * (1::nat) = n"
-  by simp
+  by (rule mult_1_right)
 
 
 subsection {* size of a datatype value *}