Structure native_ieeeLib


Source File Identifier index Theory binding index

signature native_ieeeLib =
sig
   val floatToReal : Term.term -> real
   val wordToReal  : Term.term -> real
   val realToFloat : real -> Term.term
   val realToWord  : real -> Term.term
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14