author | wenzelm |
Mon, 18 Apr 2016 15:40:41 +0200 | |
changeset 63014 | 6fff9774e088 |
parent 63013 | 37a74da77be7 |
child 63015 | 15e6ae52e91a |
--- a/src/HOL/ex/Functions.thy Mon Apr 18 15:13:46 2016 +0200 +++ b/src/HOL/ex/Functions.thy Mon Apr 18 15:40:41 2016 +0200 @@ -489,7 +489,7 @@ | "f4 _ _ = False" -subsubsection \<open>Polymorphic partial_function\<close> +subsubsection \<open>Polymorphic partial-function\<close> partial_function (option) f5 :: "'a list \<Rightarrow> 'a option" where