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/Integ/Presburger.thy
changeset 14353 79f9fbef9106
parent 14271 8ed6989228bb
child 14378 69c4d5997669 
--- a/src/HOL/Integ/Presburger.thy	Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/Presburger.thy	Mon Jan 12 16:51:45 2004 +0100
@@ -883,7 +883,7 @@
 next
   assume ?Q
   hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
-  with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
+  with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
   thus ?P by(simp)
 qed
isabelle