| Fri, 28 Sep 2012 16:51:58 +0200 |
wenzelm |
smarter handling of tracing messages;
|
changeset |
files
|
| Fri, 28 Sep 2012 15:45:03 +0200 |
wenzelm |
display number of tracing messages;
|
changeset |
files
|
| Fri, 28 Sep 2012 15:25:49 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 28 Sep 2012 15:05:16 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 28 Sep 2012 15:23:32 +0200 |
blanchet |
simplified simpset
|
changeset |
files
|
| Fri, 28 Sep 2012 15:14:11 +0200 |
blanchet |
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
|
changeset |
files
|
| Fri, 28 Sep 2012 13:16:10 +0200 |
traytel |
tuned tactic
|
changeset |
files
|
| Fri, 28 Sep 2012 11:46:57 +0200 |
wenzelm |
updated keywords using proper "isabelle update_keywords";
|
changeset |
files
|
| Fri, 28 Sep 2012 11:31:51 +0200 |
traytel |
tuned tactic
|
changeset |
files
|
| Fri, 28 Sep 2012 09:38:07 +0200 |
traytel |
tuned tactic
|
changeset |
files
|
| Fri, 28 Sep 2012 09:21:27 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
renamed ML file in preparation for next step
|
changeset |
files
|
| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
|
changeset |
files
|
| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
modernized example, exploiting "rep_compat" option
|
changeset |
files
|