blob: f742e1e67498c0ef2ea64cdeb53d016e9e5cf87f (
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 function_extra.lem.\<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
|
