Lem_maybe_extra.thy

chapter {* Generated by Lem from maybe_extra.lem. *}

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