# HG changeset patch
# User wenzelm
# Date 995659099 -7200
# Node ID 996bd4eb0ef366d9ae42f0c7841493e45fcaa98d
# Parent  cf7dae62d69d032f2c5e0e5a1fb8492403291798
HOL_ss: the_eq_trivial, the_sym_eq_trivial;

diff -r cf7dae62d69d -r 996bd4eb0ef3 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Jul 20 21:53:27 2001 +0200
+++ b/src/HOL/simpdata.ML	Fri Jul 20 21:58:19 2001 +0200
@@ -392,7 +392,7 @@
        imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
        disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial,
-       thm"plus_ac0.zero", thm"plus_ac0_zero_right"]
+       thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong]