Wed, 15 Feb 2006 21:34:57 +0100 |
wenzelm |
used Tactic.distinct_subgoals_tac;
|
file |
diff |
annotate
|
Fri, 10 Feb 2006 02:22:16 +0100 |
wenzelm |
Args/Attrib syntax: Context.generic;
|
file |
diff |
annotate
|
Sun, 29 Jan 2006 19:23:40 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Fri, 06 Jan 2006 18:18:16 +0100 |
wenzelm |
prep_meta_eq: reuse mk_rews of local simpset;
|
file |
diff |
annotate
|
Fri, 06 Jan 2006 15:18:20 +0100 |
wenzelm |
tuned EqSubst setup;
|
file |
diff |
annotate
|
Fri, 28 Oct 2005 16:35:40 +0200 |
haftmann |
cleaned up nth, nth_update, nth_map and nth_string functions
|
file |
diff |
annotate
|
Sat, 08 Oct 2005 20:15:34 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
file |
diff |
annotate
|
Mon, 01 Aug 2005 19:20:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 18:33:19 +0200 |
wenzelm |
added Id;
|
file |
diff |
annotate
|
Thu, 19 May 2005 01:22:53 +0200 |
dixon |
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
|
file |
diff |
annotate
|
Wed, 18 May 2005 23:04:13 +0200 |
dixon |
lucas - fixed subst in assumptions to count redexes from left to right.
|
file |
diff |
annotate
|
Fri, 13 May 2005 20:21:41 +0200 |
dixon |
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 |
dixon |
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 |
dixon |
lucas - added option to select occurance to rewrite e.g. (occ 4)
|
file |
diff |
annotate
|
Tue, 03 May 2005 02:45:55 +0200 |
dixon |
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 |
dixon |
lucas - updated to reflect isand.ML update
|
file |
diff |
annotate
|
Fri, 22 Apr 2005 15:10:42 +0200 |
dixon |
lucas - fixed a big with renaming of bound variables. Other small changes.
|
file |
diff |
annotate
|
Sun, 27 Feb 2005 00:00:40 +0100 |
dixon |
lucas - added more comments and an extra type to clarify the code.
|
file |
diff |
annotate
|
Sat, 19 Feb 2005 18:44:34 +0100 |
dixon |
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 |
paulson |
improved handling of chained facts
|
file |
diff |
annotate
|
Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|