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.
added missing mult_1_left to linarith simp rules
authorboehmes
Tue, 06 Apr 2010 10:46:28 +0200
changeset 36076 882403378a41
parent 36074 6301046146b6
child 36077 13f0e77128f8
added missing mult_1_left to linarith simp rules
src/HOL/Int.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Int.thy	Fri Apr 02 17:20:43 2010 +0200
+++ b/src/HOL/Int.thy	Tue Apr 06 10:46:28 2010 +0200
@@ -1502,7 +1502,7 @@
 lemmas int_arith_rules =
   neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
   minus_zero diff_minus left_minus right_minus
-  mult_zero_left mult_zero_right mult_Bit1 mult_1_right
+  mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right
   mult_minus_left mult_minus_right
   minus_add_distrib minus_minus mult_assoc
   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
isabelle