| Sun, 07 Sep 2014 09:49:05 +0200 |
haftmann |
explicit theory with additional, less commonly used list operations
|
changeset |
files
|
| Sun, 07 Sep 2014 09:49:01 +0200 |
haftmann |
generalized
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:36 +0200 |
haftmann |
theory about sum and product on function bodies
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:34 +0200 |
haftmann |
theory about lexicographic ordering on functions
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:32 +0200 |
haftmann |
added various facts
|
changeset |
files
|
| Fri, 05 Sep 2014 16:09:03 +0100 |
paulson |
Generalised card_length_listsum to all m
|
changeset |
files
|
| Fri, 05 Sep 2014 14:58:13 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
introduced mechanism to filter interpretations
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
changeset |
files
|
| Thu, 04 Sep 2014 14:02:37 +0200 |
hoelzl |
cleanup Wfrec; introduce dependent_wf/wellorder_choice
|
changeset |
files
|