| changeset 39198 | f967a16dfcdd |
| parent 37767 | a2b7a20d6ea3 |
| child 39302 | d7728f65b353 |
--- a/src/HOL/Limits.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Limits.thy Tue Sep 07 10:05:19 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] expand_fun_eq eventually_def .. +unfolding Rep_net_inject [symmetric] ext_iff eventually_def .. lemma eventually_True [simp]: "eventually (\<lambda>x. True) net" unfolding eventually_def