History log of /seL4-l4v-10.1.1/HOL4/src/1/DefnBase.sml
Revision Date Author Comments
# c7b36e85 15-Mar-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Up to hol.state0


# 86f479fe 29-Oct-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Provide utility in DefnBase to pull out "all" the terms in a defn


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


# 1bb5dd5f 02-Aug-2012 Michael Norrish <michael.norrish@nicta.com.au>

Adjust (and reduce) interface to ThmSetData.

The change is to add an extra string parameter to the callback
function that the client provides. This is the name of the theory
which has stored the theorems. This change prompted the changes to
computeLib, IndDefLib and DefnBase.

The reduction was to remove the ThmSetData's new function, forcing
BasicProvers to use new_exporter. This was possible because of the
extra information provided to its call-back.

I also wrote some test-cases mimicking the original problem that
Magnus and Ramana had, and prettied the warning output.

This closes #73.


# 1bc9f344 13-Jan-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Change src/bool to src/1 as a prelude to experimentation!