| #
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
|
| #
ff4d5b47 |
|
17-Sep-2019 |
hrutvik <hrutvikkanabar@yahoo.co.uk> |
Fix examples/fun-op-sem (#734)
* Fix examples/fun-op-sem
* Add examples/fun-op-sem to build sequence
* Test with --expk
* Closes #615
|
| #
5cd18f7c |
|
04-May-2016 |
Brian Campbell <Brian.Campbell@ed.ac.uk> |
Update fun-op-sem example to match 1f63d5f
|
| #
8be770c3 |
|
18-Oct-2015 |
Ramana Kumar <ramana@member.fsf.org> |
update fun-op-sem example
|
| #
d063ac90 |
|
27-Mar-2015 |
Ramana Kumar <ramana@member.fsf.org> |
update fun-op-sem type soundness example, cheats proved
|
| #
efca65d5 |
|
21-Mar-2015 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
fun-op-sem: improved file structure, more comments
|