| Wed, 31 Dec 2008 15:30:10 +0100 |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file | diff | annotate |
| Sat, 09 Aug 2008 22:43:46 +0200 |
unified Args.T with OuterLex.token, renamed some operations;
|
file | diff | annotate |
| Sun, 01 Jun 2008 17:45:43 +0200 |
fixed bug: maxidx was wrongly calculuated from term, now calculated
|
file | diff | annotate |
| Mon, 21 May 2007 19:13:38 +0200 |
add a bottom up search function
|
file | diff | annotate |
| Wed, 18 Apr 2007 16:23:31 +0200 |
Improved comments.
|
file | diff | annotate |
| Wed, 04 Apr 2007 00:11:03 +0200 |
removed obsolete sign_of/sign_of_thm;
|
file | diff | annotate |
| Mon, 18 Dec 2006 08:21:35 +0100 |
switched argument order in *.syntax lifters
|
file | diff | annotate |
| Thu, 07 Dec 2006 23:16:55 +0100 |
reorganized structure Tactic vs. MetaSimplifier;
|
file | diff | annotate |
| Wed, 29 Nov 2006 15:44:51 +0100 |
simplified method setup;
|
file | diff | annotate |
| Wed, 02 Aug 2006 22:26:41 +0200 |
normalized Proof.context/method type aliases;
|
file | diff | annotate |
| Tue, 11 Jul 2006 12:16:54 +0200 |
replaced Term.variant(list) by Name.variant(_list);
|
file | diff | annotate |
| Mon, 03 Jul 2006 17:24:45 +0200 |
fix to subst in order to allow subst when head of a term is a bound variable.
|
file | diff | annotate |
| Tue, 13 Jun 2006 15:42:19 +0200 |
Corrected search order for zippers.
|
file | diff | annotate |
| Mon, 12 Jun 2006 21:19:00 +0200 |
tuned Seq/Envir/Unify interfaces;
|
file | diff | annotate |
| Sun, 11 Jun 2006 00:28:18 +0200 |
added updated version of IsaPlanner and substitution.
|
file | diff | annotate |
| Wed, 26 Apr 2006 22:38:05 +0200 |
tuned;
|
file | diff | annotate |
| Wed, 15 Feb 2006 21:34:57 +0100 |
used Tactic.distinct_subgoals_tac;
|
file | diff | annotate |
| Fri, 10 Feb 2006 02:22:16 +0100 |
Args/Attrib syntax: Context.generic;
|
file | diff | annotate |
| Sun, 29 Jan 2006 19:23:40 +0100 |
tuned comment;
|
file | diff | annotate |
| Thu, 19 Jan 2006 21:22:08 +0100 |
setup: theory -> theory;
|
file | diff | annotate |
| Fri, 06 Jan 2006 18:18:16 +0100 |
prep_meta_eq: reuse mk_rews of local simpset;
|
file | diff | annotate |
| Fri, 06 Jan 2006 15:18:20 +0100 |
tuned EqSubst setup;
|
file | diff | annotate |
| Fri, 28 Oct 2005 16:35:40 +0200 |
cleaned up nth, nth_update, nth_map and nth_string functions
|
file | diff | annotate |
| Sat, 08 Oct 2005 20:15:34 +0200 |
minor tweaks for Poplog/PML;
|
file | diff | annotate |
| Mon, 01 Aug 2005 19:20:32 +0200 |
tuned signature;
|
file | diff | annotate |
| Fri, 17 Jun 2005 18:33:19 +0200 |
added Id;
|
file | diff | annotate |
| Thu, 19 May 2005 01:22:53 +0200 |
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
|
file | diff | annotate |
| Wed, 18 May 2005 23:04:13 +0200 |
lucas - fixed subst in assumptions to count redexes from left to right.
|
file | diff | annotate |
| Fri, 13 May 2005 20:21:41 +0200 |
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
|
file | diff | annotate |
| Fri, 06 May 2005 18:01:44 +0200 |
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
|
file | diff | annotate |
| Thu, 05 May 2005 13:21:05 +0200 |
lucas - added option to select occurance to rewrite e.g. (occ 4)
|
file | diff | annotate |
| Tue, 03 May 2005 02:45:55 +0200 |
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
|
file | diff | annotate |
| Tue, 26 Apr 2005 20:38:39 +0200 |
lucas - updated to reflect isand.ML update
|
file | diff | annotate |
| Fri, 22 Apr 2005 15:10:42 +0200 |
lucas - fixed a big with renaming of bound variables. Other small changes.
|
file | diff | annotate |
| Sun, 27 Feb 2005 00:00:40 +0100 |
lucas - added more comments and an extra type to clarify the code.
|
file | diff | annotate |
| Sat, 19 Feb 2005 18:44:34 +0100 |
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
|
file | diff | annotate |
| Wed, 02 Feb 2005 15:43:04 +0100 |
improved handling of chained facts
|
file | diff | annotate |
| Tue, 01 Feb 2005 18:01:57 +0100 |
the new subst tactic, by Lucas Dixon
|
file | diff | annotate |