equal
deleted
inserted
replaced
43 |
43 |
44 definition hsgn :: "hcomplex \<Rightarrow> hcomplex" |
44 definition hsgn :: "hcomplex \<Rightarrow> hcomplex" |
45 where "hsgn = *f* sgn" |
45 where "hsgn = *f* sgn" |
46 |
46 |
47 definition harg :: "hcomplex \<Rightarrow> hypreal" |
47 definition harg :: "hcomplex \<Rightarrow> hypreal" |
48 where "harg = *f* arg" |
48 where "harg = *f* Arg" |
49 |
49 |
50 definition \<comment> \<open>abbreviation for \<open>cos a + i sin a\<close>\<close> |
50 definition \<comment> \<open>abbreviation for \<open>cos a + i sin a\<close>\<close> |
51 hcis :: "hypreal \<Rightarrow> hcomplex" |
51 hcis :: "hypreal \<Rightarrow> hcomplex" |
52 where "hcis = *f* cis" |
52 where "hcis = *f* cis" |
53 |
53 |