--- 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]