Skip to content
Failed

Changes

Summary

  1. metadata
  2. '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
Changeset 8863:69121b19fe0a by immler:
metadata
The file was modified metadata/metadata (diff)
Changeset 8862:5fc6589cb7f2 by immler:
'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 addedthys/IEEE_Floating_Point/Double.thy
The file was addedthys/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 removedthys/IEEE_Floating_Point/Code_Float.thy