Theory Lem_function_extra

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