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