![[Jenkins]](/jenkins/static/858a1f95/images/svgs/logo.svg){kind=logo}
Summary
- metadata
- 'modernized' representation following the formalization in HOL4: former float_format is encoded in the type ('e, 'f)float, lifting to operations on machine representation word64
| The file was modified | metadata/metadata (diff) |
| The file was added | thys/IEEE_Floating_Point/Double.thy |
| The file was added | thys/IEEE_Floating_Point/FP64.thy |
| The file was modified | thys/Affine_Arithmetic/Affine_Approximation.thy (diff) |
| The file was modified | thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy (diff) |
| The file was modified | thys/IEEE_Floating_Point/IEEE.thy (diff) |
| The file was modified | thys/IEEE_Floating_Point/IEEE_Properties.thy (diff) |
| The file was modified | thys/IEEE_Floating_Point/ROOT (diff) |
| The file was modified | thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy (diff) |
| The file was modified | thys/Taylor_Models/Polynomial_Expression_Additional.thy (diff) |
| The file was modified | thys/Word_Lib/Word_Lemmas.thy (diff) |
| The file was removed | thys/IEEE_Floating_Point/Code_Float.thy |