Macros to introduce more concisely the abstract placeholders for the Java floating-point operations and conversions.
All our abstract operations and conversions are weakly constraned ACL2 functions that unconditionally return results of the appropriate types. The macros capture this boilerplate structure.
For now we only introduce abstract functions that involve the float and double value sets, not the extended-exponent value sets.
The abstract functions operate not on the tagged Java primitive values, but on their underlying (i.e. untagged) values.