19 Dec
2007
19 Dec
'07
9:38 p.m.
Hello,
Isabelle has the following definition under HOL:
consts the :: "'a option => 'a" primrec "the (Some x) = x"
I am wondering if there is anything equivalent in ML?
TIA,
George