src/HOL/Int.thy
changeset 55945 e96383acecf9
parent 55911 d00023bd3554
child 56525 b5b6ad5dc2ae
     1.1 --- a/src/HOL/Int.thy	Thu Mar 06 15:29:18 2014 +0100
     1.2 +++ b/src/HOL/Int.thy	Thu Mar 06 15:40:33 2014 +0100
     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 -  "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int"
     1.8 -  unfolding fun_rel_def cr_int_def int_def by simp
     1.9 +  "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int"
    1.10 +  unfolding rel_fun_def 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"