src/HOL/Nonstandard_Analysis/NSA.thy
changeset 63901 4ce989e962e0
parent 62479 716336f19aa9
child 64435 c93b0e6131c3
     1.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -1268,7 +1268,7 @@
     1.4  done
     1.5  
     1.6  text\<open>There is a unique real infinitely close\<close>
     1.7 -lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x \<approx> t"
     1.8 +lemma st_part_Ex1: "x \<in> HFinite ==> \<exists>!t::hypreal. t \<in> \<real> & x \<approx> t"
     1.9  apply (drule st_part_Ex, safe)
    1.10  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
    1.11  apply (auto intro!: approx_unique_real)