src/HOL/Int.thy
changeset 56525 b5b6ad5dc2ae
parent 55945 e96383acecf9
child 56889 48a745e1bde7
--- a/src/HOL/Int.thy	Thu Apr 10 17:48:18 2014 +0200
+++ b/src/HOL/Int.thy	Thu Apr 10 17:48:32 2014 +0200
@@ -78,8 +78,8 @@
     simp add: one_int.abs_eq plus_int.abs_eq)
 
 lemma int_transfer [transfer_rule]:
-  "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int"
-  unfolding rel_fun_def cr_int_def int_def by simp
+  "(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int"
+  unfolding rel_fun_def int.pcr_cr_eq cr_int_def int_def by simp
 
 lemma int_diff_cases:
   obtains (diff) m n where "z = int m - int n"