installing the plus_ac0 simprules
authorpaulson
Wed May 24 18:44:49 2000 +0200 (2000-05-24)
changeset 8955714497ad2348
parent 8954 4fbdda40bb5f
child 8956 a7c3538fc2d2
installing the plus_ac0 simprules
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Wed May 24 18:44:19 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed May 24 18:44:49 2000 +0200
     1.3 @@ -440,7 +440,8 @@
     1.4         if_True, if_False, if_cancel, if_eq_cancel,
     1.5         imp_disjL, conj_assoc, disj_assoc,
     1.6         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
     1.7 -       disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq]
     1.8 +       disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq,
     1.9 +       thm"plus_ac0.zero", thm"plus_ac0_zero_right"]
    1.10       @ ex_simps @ all_simps @ simp_thms)
    1.11       addsimprocs [defALL_regroup,defEX_regroup]
    1.12       addcongs [imp_cong]