| Tue, 28 Sep 2010 15:21:45 +0200 |
haftmann |
localized listsum
|
changeset |
files
|
| Tue, 28 Sep 2010 15:21:45 +0200 |
haftmann |
lemma listsum_conv_fold
|
changeset |
files
|
| Tue, 28 Sep 2010 15:34:30 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 28 Sep 2010 15:33:56 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Tue, 28 Sep 2010 15:32:59 +0200 |
haftmann |
dropped syntax for old primrec package
|
changeset |
files
|
| Tue, 28 Sep 2010 15:31:10 +0200 |
haftmann |
modernized session
|
changeset |
files
|
| Tue, 28 Sep 2010 13:44:06 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:58 +0200 |
bulwahn |
using SUBPROOF to ensure that rewriting is not done on the further subgoals of proof
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:57 +0200 |
bulwahn |
avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:53 +0200 |
bulwahn |
adding test case for interpretation of arguments that are predicates simply as input
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:52 +0200 |
bulwahn |
only modes but not types are used to destruct terms and types; this allows to interpret arguments that are predicates simply as input
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:51 +0200 |
bulwahn |
weakening check for higher-order relations, but adding check for consistent modes
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:51 +0200 |
bulwahn |
handling higher-order relations in output terms; improving proof procedure; added test case
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:50 +0200 |
bulwahn |
renaming use_random to use_generators in the predicate compiler
|
changeset |
files
|
| Tue, 28 Sep 2010 11:59:48 +0200 |
bulwahn |
fixed a typo that caused the preference of non-random modes to be ignored
|
changeset |
files
|