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/Basic_BNFs.thy
changeset 56077 d397030fb27e
parent 55945 e96383acecf9
child 58446 e89f57d1e46c 
--- a/src/HOL/Basic_BNFs.thy	Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Thu Mar 13 08:56:08 2014 +0100
@@ -175,7 +175,7 @@
   thus "f \<circ> x = g \<circ> x" by auto
 next
   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
-  unfolding image_def comp_def[abs_def] by auto
+    by (auto simp add: fun_eq_iff)
 next
   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
   apply (rule card_order_csum)
isabelle