Wed, 29 May 2013 18:52:35 +0200 | wenzelm | more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless); | changeset | files |
Wed, 29 May 2013 18:25:11 +0200 | wenzelm | tuned signature -- more explicit flags for low-level Thm.bicompose; | changeset | files |