blob: c77c977cb2ebea4323426218736f79730fe46316 (
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
|
(*Generated by Lem from function_extra.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_maybeTheory lem_boolTheory lem_basic_classesTheory lem_numTheory lem_functionTheory lemTheory;
val _ = numLib.prefer_num();
val _ = new_theory "lem_function_extra"
(*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*)
val _ = export_theory()
|
