HOL_ss: the_eq_trivial, the_sym_eq_trivial;
authorwenzelm
Fri Jul 20 21:58:19 2001 +0200 (2001-07-20)
changeset 11434996bd4eb0ef3
parent 11433 cf7dae62d69d
child 11435 bd1a7f53c11b
HOL_ss: the_eq_trivial, the_sym_eq_trivial;
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Jul 20 21:53:27 2001 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Jul 20 21:58:19 2001 +0200
     1.3 @@ -392,7 +392,7 @@
     1.4         imp_disjL, conj_assoc, disj_assoc,
     1.5         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
     1.6         disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial,
     1.7 -       thm"plus_ac0.zero", thm"plus_ac0_zero_right"]
     1.8 +       thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
     1.9       @ ex_simps @ all_simps @ simp_thms)
    1.10       addsimprocs [defALL_regroup,defEX_regroup]
    1.11       addcongs [imp_cong]