| #
d0cf5b9a |
|
12-May-2019 |
Ramana Kumar <ramana@member.fsf.org> |
Add some more align theorems
|
| #
6a32fe33 |
|
12-May-2019 |
Ramana Kumar <ramana@member.fsf.org> |
Add some theorems about align
|
| #
515b0372 |
|
03-May-2019 |
Ramana Kumar <ramana@member.fsf.org> |
Add various theorems to alignmentTheory
|
| #
18b62363 |
|
11-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get src/n-bit to build given tight-equality
|
| #
b4b8e85c |
|
18-Aug-2018 |
Andreas Lööw <AndreasLoow@users.noreply.github.com> |
Don't export ERR from HolKernel
|
| #
ad24df64 |
|
19-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Remove unnecessary qualified calls to things in Theory
These are re-exported by HolKernel anyway, and we want to rebind
HolKernel for proof-recording purposes.
|
| #
feabed51 |
|
03-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A couple of extra theorems.
|
| #
aa23933d |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Opening lcsymtacs is no longer necessary.
|
| #
fda6dec3 |
|
20-Oct-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Clean src/ to remove Unicode (or to mark it as OK)
Marking Unicode as OK is done by putting the UOK tag on the same line of
the relevant file.
|
| #
13c998f1 |
|
14-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add syntax support for alignmentTheory.
|
| #
07421c10 |
|
03-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a small theory about address alignment.
This will eventually be used to rationalise examples in l3-machine-code/.
|