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/Option.thy
changeset 55467 a5c9002bc54d
parent 55466 786edc984c98
child 55518 1ddb2edf5ceb 
--- a/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -98,7 +98,7 @@
 lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
 by (cases x) auto
 
-enriched_type map_option: map_option proof -
+functor map_option: map_option proof -
   fix f g
   show "map_option f \<circ> map_option g = map_option (f \<circ> g)"
   proof
isabelle