| #
6d57e103 |
|
06-Oct-2020 |
Joseph Chan <jhlchan@gmail.com> |
Add theorems for various helper libraries.
|
| #
b02306cc |
|
17-Apr-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Some progress
However(!): grievousness of dealing with algebra/lib is making me
rethink this.
|
| #
5417af9d |
|
31-Mar-2020 |
Arve Gengelbach <arve.gengelbach@it.uu.se> |
remove lcsymtacs (github issue #666)
The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont
|
| #
b3b2a8f3 |
|
09-Nov-2019 |
jhlchan <jhlchan@gmail.com> |
AKS mechanisation (#750)
* Add to examples: AKS, with algebra and simple_complexity.
|