src/HOL/Fact.thy
changeset 35644 d20cf282342e
parent 35028 108662d50512
child 40033 84200d970bf0
--- a/src/HOL/Fact.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Fact.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -58,7 +58,7 @@
   "x >= (0::int) \<Longrightarrow> fact x >= 0"
   by (auto simp add: fact_int_def)
 
-declare TransferMorphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return: 
     transfer_nat_int_factorial transfer_nat_int_factorial_closure]
 
 lemma transfer_int_nat_factorial:
@@ -69,7 +69,7 @@
   "is_nat x \<Longrightarrow> fact x >= 0"
   by (auto simp add: fact_int_def)
 
-declare TransferMorphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return: 
     transfer_int_nat_factorial transfer_int_nat_factorial_closure]