#
32bf1e49 |
|
02-Feb-2015 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
extra semicolons removed from (some) .sig files
|
#
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!
|
#
c3823136 |
|
17-Jun-2002 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes; crud elimination.
|
#
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.
|
#
3d2f9ce3 |
|
20-Jun-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Change stemming from split of TypeBase into TypeBasePure and TypeBase.
|
#
cfdc1706 |
|
11-Apr-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modifications caused by change of TypeBase signature.
|
#
3247f774 |
|
07-Jan-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes
|
#
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.
|