| Fri, 03 Mar 2000 21:02:45 +0100 | wenzelm | added con_elim_s(olved_)tac; | changeset | files |
| Fri, 03 Mar 2000 21:01:57 +0100 | wenzelm | mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac; | changeset | files |
| Fri, 03 Mar 2000 21:00:58 +0100 | wenzelm | added multi_resolveq, resolveq_tac; | changeset | files |
| Fri, 03 Mar 2000 18:26:19 +0100 | paulson | Added Tanja's Detects and Reachability theories. Also | changeset | files |
| Fri, 03 Mar 2000 18:22:53 +0100 | paulson | improved reasoning about {} and UNIV | changeset | files |
| Fri, 03 Mar 2000 02:00:43 +0100 | wenzelm | join_rules: compatibility check; | changeset | files |
| Fri, 03 Mar 2000 01:58:57 +0100 | wenzelm | token_trans: symbol length; | changeset | files |