equal
deleted
inserted
replaced
9 theory CLim |
9 theory CLim |
10 imports CStar |
10 imports CStar |
11 begin |
11 begin |
12 |
12 |
13 (*not in simpset?*) |
13 (*not in simpset?*) |
14 declare hypreal_epsilon_not_zero [simp] |
14 declare epsilon_not_zero [simp] |
15 |
15 |
16 (*??generalize*) |
16 (*??generalize*) |
17 lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x" |
17 lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x" |
18 for x :: complex |
18 for x :: complex |
19 by (simp add: numeral_2_eq_2) |
19 by (simp add: numeral_2_eq_2) |