#
2e71524f |
|
29-Oct-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Tidy pair{Script,Theory,Simps} to have less cruft In particular, it's desirable to reduce the number of calls to augment_srw_ss outside of Script files.
|
#
bb0dcafa |
|
05-Feb-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Change "thm-names" (used in various places) to be Thy-Name record This saves on pulling things apart and looking for dots and the like. It changes the simpLib API (most significantly for the SSFRAG function which builds simpset fragments).
|
#
3f970ed8 |
|
17-Dec-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Give theorems names in simpsets This is to allow them to be removed easily. System builds on -t1, but there are still two things to be done 1. the names associated with export_rewrites calls aren't passed on to the simpsets yet 2. there is not yet an API for removing them Also, perhaps just as an interim measure, I removed the unused entrypoint for removing rewrites by pattern matching against their LHSes (simpLib.remove_theorems).
|
#
401e3992 |
|
27-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move pair, one, sum and option into one combined coretypes directory
|