Added "triv_forall_equality" to HOL_ss.
authornipkow
Fri Feb 07 14:13:20 1997 +0100 (1997-02-07)
changeset 2595548f8ed89a80
parent 2594 4743d85eace0
child 2596 3b4ad6c7726f
Added "triv_forall_equality" to HOL_ss.
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Feb 06 18:40:39 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Feb 07 14:13:20 1997 +0100
     1.3 @@ -318,7 +318,8 @@
     1.4  	FIRST'[match_tac (TrueI::refl::ps), eq_assume_tac, ematch_tac[FalseE]]);
     1.5  
     1.6  val HOL_ss = HOL_min_ss
     1.7 -      addsimps ([if_True, if_False, if_cancel,
     1.8 +      addsimps ([triv_forall_equality, (* prunes params *)
     1.9 +                 if_True, if_False, if_cancel,
    1.10  		 o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.11                   de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
    1.12          @ ex_simps @ all_simps @ simp_thms)