| Tue, 24 Aug 2010 19:55:34 +0200 | blanchet | make Mirabelle happy | changeset | files |
| Tue, 24 Aug 2010 19:19:28 +0200 | blanchet | compute names lazily; | changeset | files |
| Tue, 24 Aug 2010 18:03:43 +0200 | blanchet | clean handling of whether a fact is chained or not; | changeset | files |
| Tue, 24 Aug 2010 16:43:52 +0200 | blanchet | don't backtick facts that contain schematic variables, since this doesn't work (for some reason) | changeset | files |
| Tue, 24 Aug 2010 16:24:11 +0200 | blanchet | quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy") | changeset | files |
| Tue, 24 Aug 2010 15:29:13 +0200 | blanchet | revert this idea of automatically invoking "metisFT" when "metis" fails; | changeset | files |
| Tue, 24 Aug 2010 22:38:45 +0800 | Christian Urban | use matching of types than just equality - this is needed in nominal to cope with type variables | changeset | files |