History log of /seL4-l4v-master/HOL4/src/tfl/src/wfrecUtils.sml
Revision Date Author Comments
# 7b73c8d7 16-Jul-2010 Konrad Slind <konrad.slind@gmail.com>

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.


# 4761143b 10-Aug-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!


# edeca38f 29-May-2002 Konrad Slind <konrad.slind@gmail.com>

Fixed so that induction theorems are as general as possible. Previously,
tupled arguments in function definitions would lead to tuples of variables
in the consequent of the induction theorem. This was needlessly specific.
Some proofs will break (i.e., become shorter) as a result.


# e21bca92 19-Nov-2000 Konrad Slind <konrad.slind@gmail.com>

Upgraded tflLib to Kan.0.


# 7ec9c98e 16-Nov-2000 Michael Norrish <Michael.Norrish@nicta.com.au>

Kananaskis compatibility.


# 8b23d815 20-Mar-2000 Konrad Slind <konrad.slind@gmail.com>

Ongoing revisions. Defn has been split into a basic datastructure
and manipulations (Defn0) and the definition entrypoints (Defn).
This allows a prettyprinter for the "defn" type to be automatically
installed when the std.prelude runs. Defn0 is part of basicHol90.


# f039c49c 17-Mar-2000 Konrad Slind <konrad.slind@gmail.com>

Big re-organizational changes. Tfl and tflLib are gone ... the relevant
files are instead Defn and TotalDefn.