changeset 23358  e0b5a74d7ace 
parent 23225  591af6a2f09e 
child 23559  0de527730294 
23357:16e0ec4bcd81  23358:e0b5a74d7ace 

92 fun perhaps f x = the_default x (f x); 
92 fun perhaps f x = the_default x (f x); 
93 
93 
94 
94 
95 (* partiality *) 
95 (* partiality *) 
96 
96 
97 exception Interrupt = Interrupt; (*signals intruding execution :[*) 

98 

99 fun try f x = SOME (f x) 
97 fun try f x = SOME (f x) 
100 handle Interrupt => raise Interrupt  _ => NONE; 
98 handle Interrupt => raise Interrupt  _ => NONE; 
101 
99 
102 fun can f x = is_some (try f x); 
100 fun can f x = is_some (try f x); 
103 
101 