History log of /seL4-l4v-master/HOL4/src/coretypes/pairSimps.sml
Revision Date Author Comments
# 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