| #
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
|
| #
90dc773d |
|
28-Jun-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get fun-op-sem/for to build again
Add it to the build sequence
|
| #
49d0d7ba |
|
19-Mar-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Fix fun-op-sem example
It was broken by changes in abbreviated simplification tactics.
|
| #
8be770c3 |
|
18-Oct-2015 |
Ramana Kumar <ramana@member.fsf.org> |
update fun-op-sem example
|
| #
efca65d5 |
|
21-Mar-2015 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
fun-op-sem: improved file structure, more comments
|