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