src/HOL/Nat.thy
changeset 47108 2a1953f0d20d
parent 46351 4a1f743c05b2
child 47208 9a91b163bb71
     1.1 --- a/src/HOL/Nat.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  One_nat_def [simp, code_post]: "1 = Suc 0"
     1.8 +  One_nat_def [simp]: "1 = Suc 0"
     1.9  
    1.10  primrec times_nat where
    1.11    mult_0:     "0 * n = (0\<Colon>nat)"
    1.12 @@ -1782,4 +1782,6 @@
    1.13  code_modulename Haskell
    1.14    Nat Arith
    1.15  
    1.16 +hide_const (open) of_nat_aux
    1.17 +
    1.18  end