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/UNITY/Rename.thy
changeset 63807 5f77017055a3
parent 63146 f1ecba0272f9 
--- a/src/HOL/UNITY/Rename.thy	Mon Sep 05 23:11:00 2016 +0200
+++ b/src/HOL/UNITY/Rename.thy	Mon Sep 05 23:39:15 2016 +0200
@@ -10,7 +10,7 @@
 definition rename :: "['a => 'b, 'a program] => 'b program" where
     "rename h == extend (%(x,u::unit). h x)"
 
-declare image_inv_f_f [simp] image_surj_f_inv_f [simp]
+declare image_inv_f_f [simp] image_f_inv_f [simp]
 
 declare Extend.intro [simp,intro]
isabelle