Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified fact references
authorhaftmann
Sun, 16 Oct 2016 13:47:35 +0200
changeset 64248 690eb1ae8bb0
parent 64247 f537616459e6
child 64249 a3f654f9a46c
simplified fact references
src/HOL/Groebner_Basis.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:33 2016 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:35 2016 +0200
@@ -51,7 +51,7 @@
 \<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
 
 declare dvd_def[algebra]
-declare dvd_eq_mod_eq_0[symmetric, algebra]
+declare mod_eq_0_iff_dvd[algebra]
 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare div_by_0[algebra]
isabelle