| #
ad57a8a3 |
|
10-Mar-2006 |
Konrad Slind <konrad.slind@gmail.com> |
Upgrading Define so that it proves more termination goals.
Generates lex. combinations and tries them out, so gets
some more ordinary recursions. Gets all iterated primitive
recursions. Also has been taught about some operations
on words (so recursion from w to w-1w will terminate,
for example).
Let me know of any bugs/slowdowns, etc.
|
| #
cb447520 |
|
20-Oct-2004 |
Konrad Slind <konrad.slind@gmail.com> |
added a development of breadth-first search.
|
| #
39a6e7cf |
|
16-Jun-2002 |
Konrad Slind <konrad.slind@gmail.com> |
Fixes to the induction theorems that TFL produces. Changes to recInduct
to reflect this. Other minor changes.
|
| #
8e6c6a10 |
|
09-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
New additions to proplog - CNF plus a few trivial proofs.
nested.scheme gives a solution to a problem posed by Paulson in
his "ML for The Working Programmer Book".
|
| #
563ab73c |
|
08-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Trivia.
|
| #
aa58d4e3 |
|
08-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Polishing.
|
| #
dd420da6 |
|
07-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Faffing about continues.
|
| #
7c006813 |
|
08-Nov-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Old and new examples that should be tucked away before I lose them again.
|