changeset 29804 | e15b74577368 |
parent 29668 | 33ba3faeaa0e |
29803:c56a5571f60a | 29804:e15b74577368 |
---|---|
1 theory ComputeNumeral |
1 theory ComputeNumeral |
2 imports ComputeHOL Float |
2 imports ComputeHOL ComputeFloat |
3 begin |
3 begin |
4 |
4 |
5 (* normalization of bit strings *) |
5 (* normalization of bit strings *) |
6 lemmas bitnorm = normalize_bin_simps |
6 lemmas bitnorm = normalize_bin_simps |
7 |
7 |