Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. finite precision computation to determine sign for comparison
  2. positive precision for truncate; fixed precision for approximation of rationals; code for truncate
  3. compute_real_of_float has not been used as code equation
Changeset 62421:28d2c75dd180 by immler:
finite precision computation to determine sign for comparison
The file was modified src/HOL/Library/Float.thy (diff)
Changeset 62420:c7666166c24e by immler:
positive precision for truncate; fixed precision for approximation of rationals; code for truncate
The file was modified src/HOL/Library/Float.thy (diff)
Changeset 62419:c7d6f4dded19 by immler:
compute_real_of_float has not been used as code equation
The file was modified src/HOL/Library/Float.thy (diff)