src/Provers/hypsubst.ML
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
less more (0) -10 -7 tip