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/ex/Simproc_Tests.thy
changeset 64240 eabf80376aab
parent 63680 6e1e8b5abbfa
child 66806 a4e82b58d833 
--- a/src/HOL/ex/Simproc_Tests.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -361,7 +361,7 @@
     have "(k) / (k*y) = uu"
       by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
   next
-    assume "(if b = 0 then 0 else a * c / 1) = uu"
+    assume "(if b = 0 then 0 else a * c) = uu"
     have "(a*(b*c)) / b = uu"
       by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
   next
isabelle