Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/simpdata.ML
changeset 14430 5cb24165a2e1
parent 13743 f8f9393be64c
child 14749 9ccfd0f59e11 
--- a/src/HOL/simpdata.ML	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/simpdata.ML	Thu Mar 04 12:06:07 2004 +0100
@@ -246,7 +246,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,
-       thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
+       thm "the_eq_trivial", the_sym_eq_trivial]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong]
isabelle