src/HOL/Nonstandard_Analysis/NSCA.thy
changeset 63901 4ce989e962e0
parent 62479 716336f19aa9
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -350,7 +350,7 @@
     1.4  apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
     1.5  done
     1.6  
     1.7 -lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x \<approx> t"
     1.8 +lemma stc_part_Ex1: "x:HFinite ==> \<exists>!t. t \<in> SComplex &  x \<approx> t"
     1.9  apply (drule stc_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_complex)