| Mon, 11 Nov 2013 10:23:01 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 11 Nov 2013 10:10:28 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
changeset |
files
|
| Sun, 10 Nov 2013 10:02:34 +0100 |
haftmann |
dropped obsolete check: dest_num always yields positive number
|
changeset |
files
|
| Sun, 10 Nov 2013 10:02:34 +0100 |
haftmann |
simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
|
changeset |
files
|
| Fri, 08 Nov 2013 21:40:07 +0100 |
nipkow |
more exercises
|
changeset |
files
|
| Fri, 08 Nov 2013 19:03:14 +0100 |
blanchet |
by (auto ...)[1] not by (auto [1])
|
changeset |
files
|
| Fri, 08 Nov 2013 08:59:54 +0100 |
nipkow |
added exercise
|
changeset |
files
|
| Thu, 07 Nov 2013 16:08:19 +1100 |
kleing |
Add output translation for <a := .., b := .., ..> state notation.
|
changeset |
files
|
| Thu, 07 Nov 2013 02:42:20 +0100 |
blanchet |
reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)
|
changeset |
files
|
| Thu, 07 Nov 2013 01:01:04 +0100 |
blanchet |
more docs
|
changeset |
files
|
| Thu, 07 Nov 2013 00:37:18 +0100 |
blanchet |
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
|
changeset |
files
|
| Wed, 06 Nov 2013 23:05:44 +0100 |
blanchet |
reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP
|
changeset |
files
|
| Wed, 06 Nov 2013 22:50:12 +0100 |
blanchet |
simplified code
|
changeset |
files
|
| Wed, 06 Nov 2013 22:42:54 +0100 |
blanchet |
fourth attempt at generalizing N2M types (to leverage caching)
|
changeset |
files
|