equal
deleted
inserted
replaced
1 (* Title: HOL/Real/Float.thy |
1 (* Title: HOL/Real/Float.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Steven Obua |
3 Author: Steven Obua |
4 *) |
4 *) |
5 |
5 |
6 theory Float = Real: |
6 theory Float imports Real begin |
7 |
7 |
8 constdefs |
8 constdefs |
9 pow2 :: "int \<Rightarrow> real" |
9 pow2 :: "int \<Rightarrow> real" |
10 "pow2 a == if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a))))" |
10 "pow2 a == if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a))))" |
11 float :: "int * int \<Rightarrow> real" |
11 float :: "int * int \<Rightarrow> real" |