| Mon, 30 Sep 2002 15:45:11 +0200 |
nipkow |
fixes !!-bound vars in induction statement automatically
|
file |
diff |
annotate
|
| Fri, 26 Jul 2002 21:09:39 +0200 |
wenzelm |
support for split assumptions in cases (hyps vs. prems);
|
file |
diff |
annotate
|
| Fri, 31 May 2002 18:49:31 +0200 |
berghofe |
Changed interface of MetaSimplifier.rewrite_term.
|
file |
diff |
annotate
|
| Tue, 07 May 2002 14:26:32 +0200 |
wenzelm |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2002 19:17:15 +0100 |
wenzelm |
cases: really append cases_default;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 21:02:18 +0100 |
wenzelm |
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 00:38:11 +0100 |
wenzelm |
join_rules RuleCases.save;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2001 20:46:05 +0100 |
wenzelm |
induct method: localize rews for rule;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2001 23:30:16 +0100 |
wenzelm |
induct: rule_versions produces localized variants;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2001 20:23:24 +0100 |
wenzelm |
proper handling of mutual rules (esp. for sets);
|
file |
diff |
annotate
|
| Mon, 05 Nov 2001 20:56:29 +0100 |
wenzelm |
Method.trace ctxt;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2001 01:28:39 +0100 |
wenzelm |
induct: internalize ``missing'' consumes-facts from goal state
|
file |
diff |
annotate
|
| Tue, 30 Oct 2001 17:30:21 +0100 |
wenzelm |
induct: cases are extracted from rulified rule;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 17:56:12 +0200 |
wenzelm |
dest_env: norm_term on rhs;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 00:32:01 +0200 |
wenzelm |
simplified resolveq_cases_tac for cases, separate version for induct;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 20:35:10 +0200 |
wenzelm |
Tactic.rewrite_cterm;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:15:07 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:05:42 +0200 |
wenzelm |
use ObjectLogic stuff;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 12:13:31 +0200 |
wenzelm |
removed vars_of, concls_of;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:20:40 +0200 |
wenzelm |
proof by cases and induction on types and sets (used to be specific for HOL);
|
file |
diff |
annotate
|