History log of /seL4-l4v-master/HOL4/examples/algebra/polynomial/polyRingScript.sml
Revision Date Author Comments
# 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.