src/HOL/ex/Functions.thy
changeset 63014 6fff9774e088
parent 62999 65f279853449
child 63067 0a8a75e400da
equal deleted inserted replaced
63013:37a74da77be7 63014:6fff9774e088
   487 where
   487 where
   488   "f4 0 0 = True"
   488   "f4 0 0 = True"
   489 | "f4 _ _ = False"
   489 | "f4 _ _ = False"
   490 
   490 
   491 
   491 
   492 subsubsection \<open>Polymorphic partial_function\<close>
   492 subsubsection \<open>Polymorphic partial-function\<close>
   493 
   493 
   494 partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
   494 partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
   495 where
   495 where
   496   "f5 x = f5 x"
   496   "f5 x = f5 x"
   497 
   497