Lem_function_extra.thy

chapter {* Generated by Lem from function_extra.lem. *}

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