src/HOL/Transfer.thy
changeset 55415 05f5fdb8d093
parent 55084 8ee9aabb2bca
child 55760 aaaccc8e015f
     1.1 --- a/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -358,12 +358,12 @@
     1.4    shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
     1.5    unfolding fun_upd_def [abs_def] by transfer_prover
     1.6  
     1.7 -lemma nat_case_transfer [transfer_rule]:
     1.8 -  "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
     1.9 +lemma case_nat_transfer [transfer_rule]:
    1.10 +  "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
    1.11    unfolding fun_rel_def by (simp split: nat.split)
    1.12  
    1.13 -lemma nat_rec_transfer [transfer_rule]:
    1.14 -  "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec"
    1.15 +lemma rec_nat_transfer [transfer_rule]:
    1.16 +  "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
    1.17    unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
    1.18  
    1.19  lemma funpow_transfer [transfer_rule]: