#
2d17e828 |
|
14-Oct-2020 |
Joseph Chan <jhlchan@gmail.com> |
Update documentation.
|
#
f61a17a6 |
|
14-Oct-2020 |
Joseph Chan <jhlchan@gmail.com> |
Revise and rename theorems for consistency.
|
#
6d57e103 |
|
06-Oct-2020 |
Joseph Chan <jhlchan@gmail.com> |
Add theorems for various helper libraries.
|
#
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.
|