| Sun, 23 Sep 2007 23:00:01 +0200 |
wenzelm |
made smlnj happy;
|
changeset |
files
|
| Sun, 23 Sep 2007 22:23:37 +0200 |
wenzelm |
tuned @{cpat};
|
changeset |
files
|
| Sun, 23 Sep 2007 22:23:35 +0200 |
wenzelm |
added read_term_pattern/schematic/abbrev;
|
changeset |
files
|
| Sun, 23 Sep 2007 22:23:34 +0200 |
wenzelm |
ProofContext.read_term_pattern;
|
changeset |
files
|
| Sun, 23 Sep 2007 22:23:33 +0200 |
wenzelm |
constrain: canonical argument order;
|
changeset |
files
|
| Sun, 23 Sep 2007 22:23:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 23 Sep 2007 22:23:27 +0200 |
wenzelm |
TypeInfer.constrain: canonical argument order;
|
changeset |
files
|
| 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
|