| changeset 39198 | f967a16dfcdd |
| parent 38968 | e55deaa22fff |
| child 39272 | 0b61951d2682 |
--- a/src/HOL/Library/Efficient_Nat.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Sep 07 10:05:19 2010 +0200 @@ -79,7 +79,7 @@ lemma [code, code_unfold]: "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))" - by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc) + by (auto simp add: ext_iff dest!: gr0_implies_Suc) subsection {* Preprocessors *}