History log of /seL4-l4v-10.1.1/HOL4/src/1/theory_tests/github130Lib.sml
Revision Date Author Comments
# 2c29276d 04-Nov-2015 Michael Norrish <Michael.Norrish@nicta.com.au>

ThmSetData passes thms *and* names to consumers

The names were always available, but the API now changes so that
consumers get names as well as theorem values. They can ignore the
names of course. (In this context, consumers are things like the
stateful rewriter, the monotonicity rule database, the TFL congruence
rule database etc.)

This will be helpful in allowing the stateful simpset to know what its
theorems are called, which is progress with Github issue #313 (to allow
easy removal of rewrites from a call to the simplifier).


# 695a9ac9 17-Oct-2013 Michael Norrish <michael.norrish@nicta.com.au>

Test demonstrating the problem with github issue #130