diff options
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml')
| -rw-r--r-- | snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml new file mode 100644 index 00000000..6543ef87 --- /dev/null +++ b/snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml @@ -0,0 +1,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.maybe 'a*) + +val _ = export_theory() + |