src/HOL/Code_Numeral.thy
 changeset 64178 12e6c3bbb488 parent 63950 cdc1e59aa513 child 64241 430d74089d4d
```     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Oct 12 21:48:52 2016 +0200
1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Oct 12 21:48:53 2016 +0200
1.3 @@ -77,23 +77,19 @@
1.4
1.5  lemma [transfer_rule]:
1.6    "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
1.7 -  by (unfold of_nat_def [abs_def]) transfer_prover
1.8 +  by (rule transfer_rule_of_nat) transfer_prover+
1.9
1.10  lemma [transfer_rule]:
1.11    "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
1.12  proof -
1.13    have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
1.14 -    by (unfold of_int_of_nat [abs_def]) transfer_prover
1.15 +    by (rule transfer_rule_of_int) transfer_prover+
1.16    then show ?thesis by (simp add: id_def)
1.17  qed
1.18
1.19  lemma [transfer_rule]:
1.20    "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
1.21 -proof -
1.22 -  have "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
1.23 -    by transfer_prover
1.24 -  then show ?thesis by simp
1.25 -qed
1.26 +  by (rule transfer_rule_numeral) transfer_prover+
1.27
1.28  lemma [transfer_rule]:
1.29    "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
```