#
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.
|
#
b48af66d |
|
02-Sep-2020 |
Arve Gengelbach <arve.gengelbach@it.uu.se> |
fix proof of SPLIT_UNION
|
#
384d8c3c |
|
21-Jul-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Fix two further proofs broken by Abbrev changes
|
#
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.
|