# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1625254755 -3600
# Node ID 5f71c16f0b37a2d0b26a713fa06a82aaa4df56d2
# Parent  a0024852e6999b8fc2868f17c34b9a67e64610ed
arg for the nonstandard complex numbers

diff -r a0024852e699 -r 5f71c16f0b37 src/HOL/Nonstandard_Analysis/NSComplex.thy
--- a/src/HOL/Nonstandard_Analysis/NSComplex.thy	Fri Jul 02 15:54:41 2021 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy	Fri Jul 02 20:39:15 2021 +0100
@@ -45,7 +45,7 @@
   where "hsgn = *f* sgn"
 
 definition harg :: "hcomplex \<Rightarrow> hypreal"
-  where "harg = *f* arg"
+  where "harg = *f* Arg"
 
 definition  \<comment> \<open>abbreviation for \<open>cos a + i sin a\<close>\<close>
   hcis :: "hypreal \<Rightarrow> hcomplex"