src/HOL/Nonstandard_Analysis/NSCA.thy
changeset 67091 1393c2340eec
parent 63901 4ce989e962e0
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Nonstandard_Analysis/NSCA.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/NSCA.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  definition \<comment>\<open>standard part map\<close>
     1.6    stc :: "hcomplex => hcomplex" where 
     1.7 -  "stc x = (SOME r. x \<in> HFinite & r:SComplex & r \<approx> x)"
     1.8 +  "stc x = (SOME r. x \<in> HFinite \<and> r\<in>SComplex \<and> r \<approx> x)"
     1.9  
    1.10  
    1.11  subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
    1.12 @@ -63,7 +63,7 @@
    1.13  
    1.14  lemma SComplex_SReal_dense:
    1.15       "[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y  
    1.16 -      |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"
    1.17 +      |] ==> \<exists>r \<in> Reals. hcmod x< r \<and> r < hcmod y"
    1.18  apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
    1.19  done
    1.20  
    1.21 @@ -350,7 +350,7 @@
    1.22  apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
    1.23  done
    1.24  
    1.25 -lemma stc_part_Ex1: "x:HFinite ==> \<exists>!t. t \<in> SComplex &  x \<approx> t"
    1.26 +lemma stc_part_Ex1: "x\<in>HFinite \<Longrightarrow> \<exists>!t. t \<in> SComplex \<and> x \<approx> t"
    1.27  apply (drule stc_part_Ex, safe)
    1.28  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
    1.29  apply (auto intro!: approx_unique_complex)