chapter \<open>Generated by Lem from \<open>function_extra.lem\<close>.\<close>

theory "Lem_function_extra" 

imports
  Main
  "Lem_maybe"
  "Lem_bool"
  "Lem_basic_classes"
  "Lem_num"
  "Lem_function"
  "Lem"

begin 



(*open import Maybe Bool Basic_classes Num Function*)

(*open import {hol} `lemTheory`*)
(*open import {isabelle} `$LIB_DIR/Lem`*)

(* ----------------------- *)
(* getting a unique value  *)
(* ----------------------- *)

(*val THE : forall 'a. ('a -> bool) -> maybe 'a*)

end