# HG changeset patch
# User haftmann
# Date 1278073397 -7200
# Node ID 7b072f0c8bde21bae07de52e44dc9d10ce00846e
# Parent  4915de09b4d371bd3c5aca97bd43daf3723dfba5
drop unconvenient code declarations

diff -r 4915de09b4d3 -r 7b072f0c8bde src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Fri Jul 02 14:23:16 2010 +0200
+++ b/src/HOL/Library/Char_nat.thy	Fri Jul 02 14:23:17 2010 +0200
@@ -53,8 +53,6 @@
   "nibble_of_nat (n mod 16) = nibble_of_nat n"
   unfolding nibble_of_nat_def mod_mod_trivial ..
 
-lemmas [code] = nibble_of_nat_norm [symmetric]
-
 lemma nibble_of_nat_simps [simp]:
   "nibble_of_nat  0 = Nibble0"
   "nibble_of_nat  1 = Nibble1"
@@ -74,9 +72,6 @@
   "nibble_of_nat 15 = NibbleF"
   unfolding nibble_of_nat_def by auto
 
-lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
-  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc One_nat_def]
-
 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
   by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)