Tue, 23 Dec 1997 11:39:03 +0100 |
paulson |
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
|
file |
diff |
annotate
|
Wed, 26 Nov 1997 16:49:07 +0100 |
paulson |
updated comment
|
file |
diff |
annotate
|
Wed, 12 Nov 1997 18:58:50 +0100 |
oheimb |
added thin_refl to hyp_subst_tac
|
file |
diff |
annotate
|
Thu, 06 Nov 1997 10:29:37 +0100 |
paulson |
hyp_subst_tac checks if the equality has type variables and uses a suitable
|
file |
diff |
annotate
|
Tue, 22 Jul 1997 11:12:55 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
Fri, 07 Mar 1997 10:22:54 +0100 |
paulson |
Prevent permutation of assumptions in hyp_subst_tac
|
file |
diff |
annotate
|
Wed, 05 Mar 1997 10:01:57 +0100 |
paulson |
Now uses rotate_tac and eta_contract_atom for greater speed
|
file |
diff |
annotate
|
Tue, 12 Nov 1996 11:36:44 +0100 |
paulson |
Removed a call to polymorphic mem
|
file |
diff |
annotate
|
Fri, 01 Nov 1996 15:15:39 +0100 |
paulson |
Replaced min by Int.min
|
file |
diff |
annotate
|
Thu, 06 Apr 1995 11:59:34 +0200 |
lcp |
Recoded with help from Toby to use rewriting instead of the
|
file |
diff |
annotate
|
Fri, 11 Nov 1994 10:42:55 +0100 |
lcp |
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
|
file |
diff |
annotate
|
Wed, 02 Nov 1994 12:44:03 +0100 |
lcp |
Provers/hypsubst: greatly simplified! No longer simulates a
|
file |
diff |
annotate
|
Wed, 19 Oct 1994 09:48:13 +0100 |
lcp |
new comments explaining abandoned change
|
file |
diff |
annotate
|
Tue, 18 Jan 1994 16:37:12 +0100 |
lcp |
Updated refs to old Sign functions
|
file |
diff |
annotate
|
Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|