src/HOL/Limits.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 41970 47d6e13d1710
     1.1 --- a/src/HOL/Limits.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Limits.thy	Mon Sep 13 11:13:15 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] ext_iff eventually_def ..
     1.8 +unfolding Rep_net_inject [symmetric] fun_eq_iff eventually_def ..
     1.9  
    1.10  lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
    1.11  unfolding eventually_def