Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Target_Numeral.thy
changeset 48075 ec5e62b868eb
parent 48073 1b609a7837ef
child 49834 b27bbb021df1 
--- a/src/HOL/Library/Target_Numeral.thy	Tue Jun 05 07:11:49 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy	Tue Jun 05 10:12:54 2012 +0200
@@ -661,30 +661,30 @@
   by (simp add: Target_Numeral.int_eq_iff)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m + n) = Target_Numeral.of_nat m + Target_Numeral.of_nat n"
+  "Target_Numeral.of_nat (m + n) = of_nat m + 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 (Target_Numeral.of_nat n)"
+  "Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (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 (Target_Numeral.of_nat m - Target_Numeral.of_nat n)"
+  "Target_Numeral.of_nat (m - n) = max 0 (of_nat m - of_nat n)"
   by (simp add: Target_Numeral.int_eq_iff)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m * n) = Target_Numeral.of_nat m * Target_Numeral.of_nat n"
+  "Target_Numeral.of_nat (m * n) = of_nat m * of_nat n"
   by (simp add: Target_Numeral.int_eq_iff of_nat_mult)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m div n) = Target_Numeral.of_nat m div Target_Numeral.of_nat n"
+  "Target_Numeral.of_nat (m div n) = of_nat m div of_nat n"
   by (simp add: Target_Numeral.int_eq_iff zdiv_int)
 
 lemma [code abstract]:
-  "Target_Numeral.of_nat (m mod n) = Target_Numeral.of_nat m mod Target_Numeral.of_nat n"
+  "Target_Numeral.of_nat (m mod n) = of_nat m mod of_nat n"
   by (simp add: Target_Numeral.int_eq_iff zmod_int)
 
 lemma [code]:
@@ -704,7 +704,7 @@
   by (simp add: less_int_def)
 
 lemma num_of_nat_code [code]:
-  "num_of_nat = Target_Numeral.num_of_int \<circ> Target_Numeral.of_nat"
+  "num_of_nat = Target_Numeral.num_of_int \<circ> of_nat"
   by (simp add: fun_eq_iff num_of_int_def of_nat_def)
 
 lemma (in semiring_1) of_nat_code:
isabelle