#
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
|
#
9524847d |
|
10-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove some duplicates of the theorem TRUTH. These are: • INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings) • IN_APP_applied and IN_ABS_applied (inadvertently generated) Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT). These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").
|
#
09673d25 |
|
04-May-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Make the zipper example look a little prettier. - Use Datatype instead of Hol_datatype - Use [simp] annotations instead of export_rewrites - Overload zapply to <*>
|
#
980cf882 |
|
25-Mar-2014 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Prove that the zipper type is what Haskell folk would call "applicative".
|
#
dc7ec111 |
|
24-Feb-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
A new example demonstrating the zipper datatype (over lists) Partly inspired by a challenge from Tony Morris
|