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.
more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
authorboehmes
Wed, 17 Aug 2016 10:23:49 +0200
changeset 63711 e4843a8a8b18
parent 63708 77323d963ca4
child 63712 2606e8c8487d
more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
src/HOL/Rat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Rat.thy	Tue Aug 16 20:54:37 2016 +0200
+++ b/src/HOL/Rat.thy	Wed Aug 17 10:23:49 2016 +0200
@@ -655,6 +655,7 @@
       @{thm divide_1}, @{thm divide_zero_left},
       @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
+      @{thm add_divide_distrib}, @{thm diff_divide_distrib},
       @{thm of_int_minus}, @{thm of_int_diff},
       @{thm of_int_of_nat_eq}]
   #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor]
isabelle