#
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).
|