| Wed, 29 Sep 2010 09:08:01 +0200 |
haftmann |
fact listsum now names listsum_foldl
|
changeset |
files
|
| Wed, 29 Sep 2010 09:08:00 +0200 |
haftmann |
delete code lemma explicitly
|
changeset |
files
|
| Wed, 29 Sep 2010 09:07:58 +0200 |
haftmann |
moved old_primrec source to nominal package, where it is still used
|
changeset |
files
|
| Tue, 28 Sep 2010 15:39:59 +0200 |
haftmann |
dropped old primrec package
|
changeset |
files
|
| Tue, 28 Sep 2010 15:34:47 +0200 |
haftmann |
merged
|
changeset |
files
|
| 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
|