# HG changeset patch
# User haftmann
# Date 1335599701 -7200
# Node ID d402ac2288b877ccb88b812ae12ee1e2c14dfc85
# Parent  151d137f1095e2100f58cdfabdaa15c978cf362b
rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly

diff -r 151d137f1095 -r d402ac2288b8 src/HOL/Library/Target_Numeral.thy
--- a/src/HOL/Library/Target_Numeral.thy	Sat Apr 28 07:38:22 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy	Sat Apr 28 09:55:01 2012 +0200
@@ -657,30 +657,30 @@
   by (simp add: Target_Numeral.int_eq_iff)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m + n) = of_nat m + of_nat n"
+  "Target_Numeral.of_nat (m + n) = Target_Numeral.of_nat m + Target_Numeral.of_nat n"
   by (simp add: Target_Numeral.int_eq_iff)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (of_nat n)"
+  "Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (Target_Numeral.of_nat n)"
   by (simp add: Target_Numeral.int_eq_iff Code_Nat.dup_def)
 
 lemma [code, code del]:
   "Code_Nat.sub = Code_Nat.sub" ..
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m - n) = max 0 (of_nat m - of_nat n)"
+  "Target_Numeral.of_nat (m - n) = max 0 (Target_Numeral.of_nat m - Target_Numeral.of_nat n)"
   by (simp add: Target_Numeral.int_eq_iff)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m * n) = of_nat m * of_nat n"
+  "Target_Numeral.of_nat (m * n) = Target_Numeral.of_nat m * Target_Numeral.of_nat n"
   by (simp add: Target_Numeral.int_eq_iff of_nat_mult)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m div n) = of_nat m div of_nat n"
+  "Target_Numeral.of_nat (m div n) = Target_Numeral.of_nat m div Target_Numeral.of_nat n"
   by (simp add: Target_Numeral.int_eq_iff zdiv_int)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m mod n) = of_nat m mod of_nat n"
+  "Target_Numeral.of_nat (m mod n) = Target_Numeral.of_nat m mod Target_Numeral.of_nat n"
   by (simp add: Target_Numeral.int_eq_iff zmod_int)
 
 lemma [code]:
@@ -735,3 +735,4 @@
   by (simp add: of_nat_def of_int_of_nat max_def)
 
 end
+