(*Generated by Lem from function_extra.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_maybeTheory lem_boolTheory lem_basic_classesTheory lem_numTheory lem_functionTheory lemTheory;

val _ = numLib.prefer_num();



val _ = new_theory "lem_function_extra"



(*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*)

val _ = export_theory()