| #
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
|
| #
d2703720 |
|
13-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rationalise eq fns in boolLib to have _eq suffix
Exception is Teq and Feq, which are not eq functions (binary
relations), but are actually unary predicates on terms.
|
| #
4888f523 |
|
15-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove eqtype declaration for term type
|
| #
d1bd7244 |
|
26-Mar-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Polish automation; realise my Knuth-Bendix completion wasn't complete.
|
| #
99321277 |
|
18-Mar-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More coding to find matches inside a list in Martin Ward's example.
|
| #
52b55c90 |
|
09-Mar-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial work on solving a cute confluence/normalisation exercise.
Taken from Martin Ward's "Foundations of Maths" course-notes.
|