# HG changeset patch # User paulson # Date 959186689 -7200 # Node ID 714497ad2348d3cf12a725411877332914789347 # Parent 4fbdda40bb5f2819f6f467fc383e24410a528f8d installing the plus_ac0 simprules diff -r 4fbdda40bb5f -r 714497ad2348 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed May 24 18:44:19 2000 +0200 +++ b/src/HOL/simpdata.ML Wed May 24 18:44:49 2000 +0200 @@ -440,7 +440,8 @@ if_True, if_False, if_cancel, if_eq_cancel, 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, Eps_eq, Eps_sym_eq] + disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq, + thm"plus_ac0.zero", thm"plus_ac0_zero_right"] @ ex_simps @ all_simps @ simp_thms) addsimprocs [defALL_regroup,defEX_regroup] addcongs [imp_cong]