blob: 7ed34eeb029c81750b2b17974c3ad7daff71e030 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
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
|
