| Wed, 14 Jun 2000 17:59:53 +0200 | wenzelm | theorems [cases type: bool] = case_split; | file | diff | annotate |
| Fri, 05 May 2000 22:32:25 +0200 | wenzelm | use Args.colon / Args.parens; | file | diff | annotate |
| Wed, 12 Apr 2000 23:51:57 +0200 | wenzelm | export concl_of; | file | diff | annotate |
| Wed, 12 Apr 2000 18:53:09 +0200 | wenzelm | induct stripped: match_tac; | file | diff | annotate |
| Wed, 05 Apr 2000 21:02:31 +0200 | wenzelm | HEADGOAL; | file | diff | annotate |
| Mon, 20 Mar 2000 18:48:43 +0100 | wenzelm | tuned degenerate cases / induct; | file | diff | annotate |
| Tue, 14 Mar 2000 11:33:30 +0100 | wenzelm | tuned comments; | file | diff | annotate |
| Mon, 13 Mar 2000 13:19:14 +0100 | wenzelm | export vars_of; | file | diff | annotate |
| Thu, 09 Mar 2000 22:56:40 +0100 | wenzelm | cleaned comment; | file | diff | annotate |
| Wed, 08 Mar 2000 18:08:08 +0100 | wenzelm | added dest_global/local_rules; | file | diff | annotate |
| Sat, 04 Mar 2000 13:28:21 +0100 | wenzelm | induct: "stripped" option; | file | diff | annotate |
| Fri, 03 Mar 2000 21:02:45 +0100 | wenzelm | added con_elim_s(olved_)tac; | file | diff | annotate |
| Fri, 03 Mar 2000 02:00:43 +0100 | wenzelm | join_rules: compatibility check; | file | diff | annotate |
| Thu, 02 Mar 2000 18:18:59 +0100 | wenzelm | join induct rules; | file | diff | annotate |
| Tue, 29 Feb 2000 20:51:43 +0100 | wenzelm | tuned msgs; | file | diff | annotate |
| Sun, 27 Feb 2000 15:33:35 +0100 | wenzelm | cases/induct attributes; | file | diff | annotate |
| Thu, 24 Feb 2000 16:01:34 +0100 | wenzelm | induct method: implicit rule; | file | diff | annotate |
| Tue, 22 Feb 2000 21:48:24 +0100 | wenzelm | induct: tuned syntax; | file | diff | annotate |
| Fri, 28 Jan 2000 12:12:06 +0100 | wenzelm | replaced FIRSTGOAL by FINDGOAL (backtracking!); | file | diff | annotate |
| Tue, 07 Sep 1999 18:10:33 +0200 | wenzelm | rule option; | file | diff | annotate |
| Fri, 16 Jul 1999 13:25:45 +0200 | berghofe | Replaced datatype_info by datatype_info_err. | file | diff | annotate |
| Tue, 27 Apr 1999 10:47:40 +0200 | wenzelm | support forward chaining; | file | diff | annotate |
| Fri, 16 Apr 1999 17:47:06 +0200 | wenzelm | may specify induction predicates as well; | file | diff | annotate |
| Fri, 16 Apr 1999 14:50:30 +0200 | wenzelm | Proof by induction on types / set / functions. | file | diff | annotate |