| #
55622e44 |
|
24-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get core HOL to build with new definition of "by"
Progress with github issue #407
|
| #
3f0b07e2 |
|
27-Nov-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Fix more proofs for #346
|
| #
22dff31f |
|
28-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix integer theories in light of pat_assum rename
|
| #
aa23933d |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Opening lcsymtacs is no longer necessary.
|
| #
84cc1436 |
|
13-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
All l/case short simp tacs use LET_ss + ARITH_ss
This means that fs and rfs pick up LET_ss and ARITH_ss, making them
indistinguishable from the 'l' versions.
|
| #
92317114 |
|
08-Jan-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
Change API of Q's MATCH...RENAME_TACs.
Now rather than a string list hanging off the end specifying which
variable bindings aren't supposed to induce a renaming, just put
underscores into the pattern in those positions.
Documentation and release notes updated.
|
| #
7589d772 |
|
09-May-2014 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
move int_bitwise from src/n-bit to src/integer
|