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-13