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
|