| 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 |