#
3a981fec |
|
21-Sep-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add some whitespace to signature files.
|
#
161d7acc |
|
02-Jul-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Floating-point update. • isSignallingNan predicate is added to machine_ieeeTheory. • The RISC-V model is simplified in places (for DIV and REM). • The L3 import is extended to cover more operations.
|
#
086cbeb8 |
|
22-Jun-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor changes within floating-point theory. • The operations float_negate1985 and float_abs1985 have been removed. • Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan. • Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.
|
#
d34415b5 |
|
02-May-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for latest L3. Removes some unnecessary bracketing.
|
#
e3deee9f |
|
11-Apr-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update RISC-V SML code. Should have been included with commit 4b08982.
|
#
5835e692 |
|
27-May-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add SML version of RISC-V model.
|