| Wed, 22 Mar 2000 12:33:34 +0100 |
paulson |
new meta-rule "inst", a shorthand for read_instantiate_sg
|
file |
diff |
annotate
|
| Fri, 17 Mar 2000 16:28:59 +0100 |
wenzelm |
untag: remove all tags of given name;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2000 14:57:06 +0100 |
berghofe |
Type.unify and Type.typ_match now use Vartab instead of association lists.
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 17:49:28 +0100 |
wenzelm |
added (un)tag_rule;
|
file |
diff |
annotate
|
| Thu, 02 Mar 2000 18:18:10 +0100 |
wenzelm |
added freeze_all;
|
file |
diff |
annotate
|
| Mon, 17 Jan 2000 14:10:32 +0100 |
paulson |
Thm.instantiate no longer normalizes, but Drule.instantiate does
|
file |
diff |
annotate
|
| Wed, 05 Jan 2000 11:35:18 +0100 |
wenzelm |
TypeInfer.logicT;
|
file |
diff |
annotate
|
| Thu, 21 Oct 1999 18:41:51 +0200 |
wenzelm |
forall_elim_var(s) moved to pure_thy.ML;
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 13:50:48 +0200 |
wenzelm |
strip_shyps_warning;
|
file |
diff |
annotate
|
| Sat, 04 Sep 1999 20:59:33 +0200 |
wenzelm |
handle Bind!!
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:04:01 +0200 |
wenzelm |
PureThy.smart_store_thms;
|
file |
diff |
annotate
|
| Fri, 27 Aug 1999 18:59:27 +0200 |
wenzelm |
thm "_" = asm_rl;
|
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
|
| Tue, 13 Jul 1999 13:53:34 +0200 |
wenzelm |
added mk_cgoal, assume_goal;
|
file |
diff |
annotate
|
| Fri, 09 Jul 1999 16:54:54 +0200 |
wenzelm |
added compose_single;
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 18:31:04 +0200 |
wenzelm |
improved error msgs of cterm_instantiate;
|
file |
diff |
annotate
|
| Fri, 16 Apr 1999 14:42:44 +0200 |
wenzelm |
added incr_indexes, incr_indexes_wrt;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:00 +0100 |
wenzelm |
qualify Theory.sign_of etc.;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 12:30:42 +0100 |
wenzelm |
added rule_attribute: ('a -> thm -> thm) -> 'a attribute;
|
file |
diff |
annotate
|
| Tue, 17 Nov 1998 14:05:47 +0100 |
wenzelm |
export vars_of and friends;
|
file |
diff |
annotate
|
| Tue, 20 Oct 1998 16:29:08 +0200 |
wenzelm |
added unvarify(T);
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 17:43:00 +0200 |
paulson |
Rule mk_triv_goal for making instances of triv_goal
|
file |
diff |
annotate
|
| Thu, 25 Jun 1998 15:20:59 +0200 |
wenzelm |
added rewrite_cterm;
|
file |
diff |
annotate
|
| Sat, 04 Apr 1998 11:42:48 +0200 |
wenzelm |
added triv_goal, rev_triv_goal (for Isar);
|
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:08:06 +0100 |
wenzelm |
Syntax.indexname;
|
file |
diff |
annotate
|
| Wed, 04 Mar 1998 13:16:05 +0100 |
nipkow |
Reorganized simplifier. May now reorient rules.
|
file |
diff |
annotate
|
| Sat, 07 Feb 1998 14:39:35 +0100 |
paulson |
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
|
file |
diff |
annotate
|
| Fri, 30 Jan 1998 11:32:19 +0100 |
wenzelm |
removed dead messy code;
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:13:47 +0100 |
wenzelm |
adapted to new sort function;
|
file |
diff |
annotate
|