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/HOLCF/Cfun.thy
changeset 49759 ecf1d5d87e5e
parent 45695 b108b3d7c49e
child 51717 9e7d1c139569 
--- a/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -15,7 +15,7 @@
 
 definition "cfun = {f::'a => 'b. cont f}"
 
-cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
+cpodef ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
   unfolding cfun_def by (auto intro: cont_const adm_cont)
 
 type_notation (xsymbols)
isabelle