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/Transfer_Int_Nat.thy
changeset 67118 ccab07d1196c
parent 66954 0230af0f3c59
child 67399 eab6ce8368fa 
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -86,7 +86,7 @@
   unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
-  unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
   unfolding rel_fun_def ZN_def by (simp add: zdiv_int)
isabelle