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