Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arg for the nonstandard complex numbers
authorpaulson <lp15@cam.ac.uk>
Fri, 02 Jul 2021 20:39:15 +0100
changeset 73926 5f71c16f0b37
parent 73925 a0024852e699
child 73927 5b5e015189a4
arg for the nonstandard complex numbers
src/HOL/Nonstandard_Analysis/NSComplex.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle