| changeset 39302 | d7728f65b353 |
| parent 39198 | f967a16dfcdd |
| child 41970 | 47d6e13d1710 |
--- a/src/HOL/Limits.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Limits.thy Mon Sep 13 11:13:15 2010 +0200 @@ -46,7 +46,7 @@ lemma expand_net_eq: shows "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')" -unfolding Rep_net_inject [symmetric] ext_iff eventually_def .. +unfolding Rep_net_inject [symmetric] fun_eq_iff eventually_def .. lemma eventually_True [simp]: "eventually (\<lambda>x. True) net" unfolding eventually_def