diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Nonstandard_Analysis/NSCA.thy --- a/src/HOL/Nonstandard_Analysis/NSCA.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Nonstandard_Analysis/NSCA.thy Sun Nov 26 21:08:32 2017 +0100 @@ -16,7 +16,7 @@ definition \\standard part map\ stc :: "hcomplex => hcomplex" where - "stc x = (SOME r. x \ HFinite & r:SComplex & r \ x)" + "stc x = (SOME r. x \ HFinite \ r\SComplex \ r \ x)" subsection\Closure Laws for SComplex, the Standard Complex Numbers\ @@ -63,7 +63,7 @@ lemma SComplex_SReal_dense: "[| x \ SComplex; y \ SComplex; hcmod x < hcmod y - |] ==> \r \ Reals. hcmod x< r & r < hcmod y" + |] ==> \r \ Reals. hcmod x< r \ r < hcmod y" apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex) done @@ -350,7 +350,7 @@ apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard]) done -lemma stc_part_Ex1: "x:HFinite ==> \!t. t \ SComplex & x \ t" +lemma stc_part_Ex1: "x\HFinite \ \!t. t \ SComplex \ x \ t" apply (drule stc_part_Ex, safe) apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) apply (auto intro!: approx_unique_complex)