src/HOL/Library/Code_Abstract_Nat.thy
changeset 55415 05f5fdb8d093
parent 51113 222fb6cb2c3e
child 55757 9fc71814b8c1
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4  *}
     1.5  
     1.6  lemma [code, code_unfold]:
     1.7 -  "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
     1.8 +  "case_nat = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
     1.9    by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
    1.10  
    1.11