diff options
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_maybe_extra.thy')
| -rw-r--r-- | snapshots/isabelle/lib/lem/Lem_maybe_extra.thy | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_maybe_extra.thy b/snapshots/isabelle/lib/lem/Lem_maybe_extra.thy new file mode 100644 index 00000000..0a57814c --- /dev/null +++ b/snapshots/isabelle/lib/lem/Lem_maybe_extra.thy @@ -0,0 +1,24 @@ +chapter \<open>Generated by Lem from maybe_extra.lem.\<close> + +theory "Lem_maybe_extra" + +imports + Main + "Lem_basic_classes" + "Lem_maybe" + "Lem_assert_extra" + +begin + + + +(*open import Basic_classes Maybe Assert_extra*) + +(* ----------------------- *) +(* fromJust *) +(* ----------------------- *) + +(*val fromJust : forall 'a. maybe 'a -> 'a*) +(*let fromJust op= match op with | Just v -> v | Nothing -> failwith fromJust of Nothing end*) + +end |