| Tue, 07 May 2002 14:26:32 +0200 |
wenzelm |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
file |
diff |
annotate
|
| Thu, 24 Jan 2002 22:42:14 +0100 |
wenzelm |
fixed subgoal_tac; fails on non-existent subgoal;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 21:03:29 +0100 |
wenzelm |
renamed norm_hhf to norm_hhf_rule;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 22:24:37 +0100 |
wenzelm |
tune norm_hhf_tac;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2001 11:52:54 +0100 |
wenzelm |
changed Thm.varifyT';
|
file |
diff |
annotate
|
| Thu, 29 Nov 2001 00:44:34 +0100 |
wenzelm |
general type of delete_tagged_brl;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 18:36:07 +0100 |
wenzelm |
prove: raise ERROR_MESSAGE;
|
file |
diff |
annotate
|
| Tue, 13 Nov 2001 17:51:03 +0100 |
wenzelm |
prove: Envir.beta_norm;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2001 21:31:52 +0100 |
wenzelm |
added conjunction_tac;
|
file |
diff |
annotate
|
| Sun, 28 Oct 2001 19:44:26 +0100 |
wenzelm |
tuned prove;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2001 23:19:04 +0200 |
wenzelm |
tuned prove;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2001 00:07:19 +0200 |
wenzelm |
prove: primitive goal interface for internal use;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 02:12:10 +0200 |
wenzelm |
innermost_params;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 20:31:52 +0200 |
wenzelm |
qualify some names;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:05:46 +0200 |
wenzelm |
unified rewrite/rewrite_cterm/simplify interface;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:08:42 +0200 |
wenzelm |
tuned full_rewrite;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:21:17 +0200 |
wenzelm |
added full_rewrite_cterm;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:36:11 +0100 |
wenzelm |
tuned norm_hhf(_tac);
|
file |
diff |
annotate
|
| Sat, 06 Jan 2001 21:27:12 +0100 |
wenzelm |
added norm_hhf(_tac);
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:12:30 +0100 |
wenzelm |
added rewrite_goal_tac;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2000 17:50:21 +0100 |
berghofe |
moved rewriting functions from Drule to MetaSimplifier
|
file |
diff |
annotate
|
| Fri, 27 Oct 2000 15:53:47 +0200 |
oheimb |
added instantiate_tac
|
file |
diff |
annotate
|
| Fri, 04 Aug 2000 22:59:08 +0200 |
wenzelm |
added rename_params_tac;
|
file |
diff |
annotate
|
| Thu, 25 May 2000 15:22:19 +0200 |
paulson |
res_inst_tac, etc., no longer print the "dest_state" message when the selected
|
file |
diff |
annotate
|
| Mon, 17 Jan 2000 14:10:32 +0100 |
paulson |
Thm.instantiate no longer normalizes, but Drule.instantiate does
|
file |
diff |
annotate
|
| Sat, 25 Sep 1999 13:05:38 +0200 |
wenzelm |
added fold_rule;
|
file |
diff |
annotate
|
| Mon, 06 Sep 1999 18:18:09 +0200 |
oheimb |
added ftac, eatac, datac, fatac
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 10:54:44 +0200 |
paulson |
new primitive rule permute_prems to underlie defer_tac and rotate_prems
|
file |
diff |
annotate
|