src/HOL/Real/Rational.thy

 
 instantiation rat :: number_ring
 begin
 
 definition
-  rat_number_of_def: "number_of w = (of_int w \<Colon> rat)"
+  rat_number_of_def [code func del]: "number_of w = (of_int w \<Colon> rat)"
 
 instance
   by default (simp add: rat_number_of_def)
 
 end 

 lemma Rational_lit [simp]: "Rational i\<^sub>N = rat_of_int i"
   by (simp add: Rational_simp)
 
 lemma zero_rat_code [code, code unfold]:
   "0 = Rational 0\<^sub>N" by simp
-
-lemma zero_rat_code [code, code unfold]:
+declare zero_rat_code [symmetric, code post]
+
+lemma one_rat_code [code, code unfold]:
   "1 = Rational 1\<^sub>N" by simp
-
-lemma [code, code unfold]:
+declare one_rat_code [symmetric, code post]
+
+lemma [code unfold, symmetric, code post]:
   "number_of k = rat_of_int (number_of k)"
   by (simp add: number_of_is_id rat_number_of_def)
 
 definition
   [code func del]: "Fract' (b\<Colon>bool) k l = Fract k l"