| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
permissions failure in CBuildCap.
|
|
-- an assertion failure that new bounds are exact. The address of the new cap should have address=base (i.e. offset=0) but this was not being set. This was not previously visible because all other uses of setCapBounds already have address=newBase when calling.
|
|
|
|
|
|
|
|
|
|
|
|
mono rewrites
|
|
|
|
|
|
|
|
For some reason there was a desugaring rule that mapped f((x, y)) to
f(x, y) in initial_check.ml, this prevented functions and constructors
from being applied to tuples.
|
|
|
|
|
|
|
|
|
|
|
|
Placed in lib/isabelle/manual/document.pdf
Also fixed a few typos.
|
|
|
|
|
|
|
|
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
They are used in various specs and test cases.
|
|
|
|
|
|
Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't
allow a space after the -i option.
|
|
For GNU sed, the extension is optional in
sed -i ...
But in BSD sed, the extension is mandatory
sed -i .bak ...
|
|
(note that they're already declared in lib/arith.sail)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
