Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. SMT-LIB interpretation of floating-point arithmetic
  2. merged
  3. SMT-LIB interpretation of floating-point arithmetic
  4. IEEE model with a single NaN value
  5. Minor
Changeset 13467:1a1e92696b0d by tjark weber _tjark.weber@it.uu.se_:
SMT-LIB interpretation of floating-point arithmetic
The file was addedthys/IEEE_Floating_Point/smt_float.ML
Changeset 13466:7d35d973a7a8 by tjark weber _tjark.weber@it.uu.se_:
merged
Changeset 13465:220a718edcd3 by tjark weber _tjark.weber@it.uu.se_:
SMT-LIB interpretation of floating-point arithmetic
The file was addedthys/IEEE_Floating_Point/IEEE_Single_NaN_SMTLIB.thy
The file was modified thys/IEEE_Floating_Point/ROOT
Changeset 13464:75232d03666a by tjark weber _tjark.weber@it.uu.se_:
IEEE model with a single NaN value
The file was addedthys/IEEE_Floating_Point/IEEE_Single_NaN.thy
The file was modified thys/IEEE_Floating_Point/ROOT
Changeset 13463:cf4b252d5cc5 by tjark weber _tjark.weber@it.uu.se_:
Minor
The file was modified thys/IEEE_Floating_Point/IEEE.thy
The file was modified thys/IEEE_Floating_Point/IEEE_Properties.thy