| Sun, 23 Sep 2007 22:23:24 +0200 |
wenzelm |
tuned ML setup;
|
changeset |
files
|
| Sun, 23 Sep 2007 22:11:50 +0200 |
urbanc |
tuned one proof so to not run in a loop with the new atom-representation
|
changeset |
files
|
| Sun, 23 Sep 2007 22:10:27 +0200 |
urbanc |
changed the representation of atoms to datatypes over nats
|
changeset |
files
|
| Sat, 22 Sep 2007 17:45:58 +0200 |
wenzelm |
ProofContext.mode_abbrev;
|
changeset |
files
|
| Sat, 22 Sep 2007 17:45:57 +0200 |
wenzelm |
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
|
changeset |
files
|
| Sat, 22 Sep 2007 17:45:56 +0200 |
wenzelm |
certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
|
changeset |
files
|
| Sat, 22 Sep 2007 17:45:55 +0200 |
wenzelm |
certify: do_expand as explicit argument, actually certify type of abstractions;
|
changeset |
files
|
| Fri, 21 Sep 2007 22:51:13 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Sep 2007 22:51:12 +0200 |
wenzelm |
added has_abs (from envir.ML);
|
changeset |
files
|
| Fri, 21 Sep 2007 22:51:10 +0200 |
wenzelm |
Term.has_abs;
|
changeset |
files
|
| Fri, 21 Sep 2007 22:51:08 +0200 |
wenzelm |
proper signature constraint;
|
changeset |
files
|
| Thu, 20 Sep 2007 20:58:40 +0200 |
wenzelm |
added interrupt_timeout;
|
changeset |
files
|
| Thu, 20 Sep 2007 20:56:54 +0200 |
wenzelm |
Generic interpretation of theory data.
|
changeset |
files
|
| Thu, 20 Sep 2007 20:56:34 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 20 Sep 2007 20:56:33 +0200 |
wenzelm |
avoid Theory.rep_theory;
|
changeset |
files
|