Mon, 23 Jan 2006 11:41:54 +0100 | paulson | ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first | changeset | files |
Mon, 23 Jan 2006 11:38:43 +0100 | paulson | Clausification now handles some IFs in rewrite rules (if-split did not work) | changeset | files |
Mon, 23 Jan 2006 11:37:53 +0100 | paulson | bugfix: induct_tac no longer raises THM "dest_state" | changeset | files |
Mon, 23 Jan 2006 11:36:50 +0100 | paulson | fixed the <<= notation | changeset | files |