| #
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
|
| #
18934f7c |
|
03-Dec-2018 |
Johannes Åman Pohjola <johannes.amanpohjola@data61.csiro.au> |
Reconcile store_thms with diverging names in db and val binding
|
| #
49d0d7ba |
|
19-Mar-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Fix fun-op-sem example
It was broken by changes in abbreviated simplification tactics.
|
| #
e98f8b20 |
|
20-Oct-2015 |
Ramana Kumar <ramana@member.fsf.org> |
move some things out of for_osmall into lprefix_lub
some of them should probably move further back again
|
| #
8be770c3 |
|
18-Oct-2015 |
Ramana Kumar <ramana@member.fsf.org> |
update fun-op-sem example
|