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 |
Tue, 24 Aug 2010 15:08:05 +0200 | blanchet | merge | changeset | files |
Tue, 24 Aug 2010 15:07:54 +0200 | blanchet | cosmetics | changeset | files |