| 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
|
| Mon, 12 Jul 1999 22:25:19 +0200 |
wenzelm |
removed metacuts_tac;
|
file |
diff |
annotate
|
| Sat, 10 Jul 1999 21:41:57 +0200 |
wenzelm |
defer_tac: use try for general exn handling;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:00 +0100 |
wenzelm |
qualify Theory.sign_of etc.;
|
file |
diff |
annotate
|
| Thu, 26 Nov 1998 12:18:08 +0100 |
nipkow |
Added filter_prems_tac
|
file |
diff |
annotate
|
| Wed, 25 Nov 1998 13:57:44 +0100 |
wenzelm |
replaced prs by writeln;
|
file |
diff |
annotate
|
| Mon, 09 Nov 1998 15:40:26 +0100 |
wenzelm |
added metacuts_tac;
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 10:37:33 +0200 |
wenzelm |
added solve_tac;
|
file |
diff |
annotate
|
| Tue, 10 Mar 1998 13:24:11 +0100 |
nipkow |
New simplifier flag for mutual simplification.
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:09:06 +0100 |
wenzelm |
adapted to baroque chars;
|
file |
diff |
annotate
|
| Sat, 07 Feb 1998 14:40:05 +0100 |
paulson |
moved freeze_thaw to drule.ML
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 09:58:03 +0100 |
wenzelm |
adapted to new sort function;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 16:22:10 +0100 |
wenzelm |
tuned warning msg;
|
file |
diff |
annotate
|
| Thu, 06 Nov 1997 10:28:20 +0100 |
paulson |
subgoal_tac displays a warning if the new subgoal has type variables
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:13:21 +0200 |
wenzelm |
ProtoPure.thy;
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 11:56:12 +0200 |
nipkow |
Modified comment.
|
file |
diff |
annotate
|
| Thu, 25 Sep 1997 12:09:41 +0200 |
paulson |
Generalized and exported biresolution_from_nets_tac to allow the declaration
|
file |
diff |
annotate
|
| Fri, 25 Jul 1997 11:47:09 +0200 |
wenzelm |
improved rewrite_thm / rewrite_goals to handle conditional eqns;
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 10:22:30 +0200 |
wenzelm |
tuned apsome;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:14:18 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:52:43 +0200 |
paulson |
Tidying of signature. More robust renaming in freeze_thaw.
|
file |
diff |
annotate
|
| Wed, 19 Mar 1997 10:24:39 +0100 |
paulson |
delete_tagged_brl just ignores non-elimination rules instead of complaining
|
file |
diff |
annotate
|
| Fri, 28 Feb 1997 15:46:41 +0100 |
paulson |
rule_by_tactic no longer standardizes its result
|
file |
diff |
annotate
|
| Fri, 21 Feb 1997 15:31:47 +0100 |
paulson |
Replaced "flat" by the Basis Library function List.concat
|
file |
diff |
annotate
|
| Tue, 04 Feb 1997 10:33:58 +0100 |
paulson |
Gradual switching to Basis Library functions nth, drop, etc.
|
file |
diff |
annotate
|
| Tue, 26 Nov 1996 16:18:42 +0100 |
paulson |
Eta-expansion of a function definition, for value polymorphism
|
file |
diff |
annotate
|
| Fri, 01 Nov 1996 15:30:49 +0100 |
paulson |
asm_rewrite_goal_tac now calls SELECT_GOAL.
|
file |
diff |
annotate
|
| Mon, 30 Sep 1996 10:59:47 +0200 |
paulson |
prune_params_tac no longer rewrites main goal
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 11:10:46 +0200 |
paulson |
Generalized freeze to freeze_thaw in order to
|
file |
diff |
annotate
|
| Wed, 11 Sep 1996 18:00:53 +0200 |
nipkow |
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
|
file |
diff |
annotate
|
| Mon, 09 Sep 1996 18:53:41 +0200 |
nipkow |
added cterm_lift_inst_rule
|
file |
diff |
annotate
|
| Thu, 05 Sep 1996 18:29:43 +0200 |
paulson |
Added thin_tac to signature; previous change was useless
|
file |
diff |
annotate
|
| Thu, 05 Sep 1996 10:29:52 +0200 |
paulson |
Declared thin_tac
|
file |
diff |
annotate
|
| Fri, 14 Jun 1996 12:27:11 +0200 |
paulson |
Added delete function for brls
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 12:34:18 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Fri, 28 Jul 1995 17:24:53 +0200 |
nipkow |
added rotate_tac.
|
file |
diff |
annotate
|
| Fri, 28 Apr 1995 11:52:43 +0200 |
lcp |
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
|
file |
diff |
annotate
|