| Fri, 13 Oct 2006 18:08:48 +0200 |
berghofe |
Repaired strip_assums_hyp (now also works for goals not
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:11 +0200 |
wenzelm |
removed is_equals, is_implies;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:39 +0200 |
wenzelm |
added name_classrel/arities/arity;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:03 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:47 +0200 |
wenzelm |
(un)varify: tuned exceptions;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:28 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 21:54:21 +0200 |
wenzelm |
support embedded terms;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:03 +0200 |
wenzelm |
added dest_conjunction_list;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2006 16:00:02 +0200 |
wenzelm |
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 00:33:49 +0200 |
wenzelm |
Term.itselfT;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:39 +0100 |
wenzelm |
simplified Pure conjunction, based on actual const;
|
file |
diff |
annotate
|
| Sat, 18 Feb 2006 18:08:23 +0100 |
wenzelm |
dest_def: tuned error msg;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 18:25:55 +0100 |
wenzelm |
dest_def: actually return beta-eta contracted equation;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:45 +0100 |
wenzelm |
renamed gen_duplicates to duplicates;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:05 +0100 |
wenzelm |
added generic dest_def (mostly from theory.ML);
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:23 +0100 |
wenzelm |
added dest_all;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:48 +0100 |
wenzelm |
added mk_conjunction_list2;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:28:58 +0100 |
wenzelm |
mk_conjunction: proper treatment of bounds;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 18:58:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:57 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 13:06:05 +0200 |
paulson |
optimization to incr_indexes?
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:51 +0200 |
wenzelm |
incr_tvar (from term.ML), incr_indexes: avoid garbage;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:29 +0200 |
wenzelm |
occs no longer infix (structure not open);
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:21 +0200 |
wenzelm |
added nth_prem;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2005 18:44:52 +0100 |
ballarin |
First version of global registration command.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 12:41:06 +0100 |
paulson |
thin_tac now works on P==>Q
|
file |
diff |
annotate
|
| Fri, 21 Jan 2005 13:55:07 +0100 |
paulson |
fixed thin_tac with higher-level assumptions by removing the old code to
|
file |
diff |
annotate
|