| Mon, 04 Oct 2010 15:05:19 +0200 | blanchet | apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed | changeset | files |
| Mon, 04 Oct 2010 14:36:18 +0200 | blanchet | instantiate foralls and release exists in the order described by the topological order | changeset | files |
| Mon, 04 Oct 2010 14:34:15 +0200 | blanchet | reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables | changeset | files |