src/HOL/Limits.thy
changeset 39198 f967a16dfcdd
parent 37767 a2b7a20d6ea3
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Limits.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Limits.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5  lemma expand_net_eq:
     1.6    shows "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
     1.7 -unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def ..
     1.8 +unfolding Rep_net_inject [symmetric] ext_iff eventually_def ..
     1.9  
    1.10  lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
    1.11  unfolding eventually_def