Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transfer.thy
changeset 55415 05f5fdb8d093
parent 55084 8ee9aabb2bca
child 55760 aaaccc8e015f 
--- a/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -358,12 +358,12 @@
   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
   unfolding fun_upd_def [abs_def] by transfer_prover
 
-lemma nat_case_transfer [transfer_rule]:
-  "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
+lemma case_nat_transfer [transfer_rule]:
+  "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
   unfolding fun_rel_def by (simp split: nat.split)
 
-lemma nat_rec_transfer [transfer_rule]:
-  "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec"
+lemma rec_nat_transfer [transfer_rule]:
+  "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
   unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
 
 lemma funpow_transfer [transfer_rule]:
isabelle