equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Floating-Point Numbers *} |
6 header {* Floating-Point Numbers *} |
7 |
7 |
8 theory Float |
8 theory Float |
9 imports Complex_Main |
9 imports Complex_Main Lattice_Algebras |
10 begin |
10 begin |
11 |
11 |
12 definition |
12 definition |
13 pow2 :: "int \<Rightarrow> real" where |
13 pow2 :: "int \<Rightarrow> real" where |
14 [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))" |
14 [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))" |