I am not quite sure whether I get your question. First, the syntax of Isabelle/HOL and SML is not very different. If you just want to get variants of your function in SML, probably the fastest way is using Isabelle's code generator
export_code del1 delall in SML
which results in something like
fun del1 A_ a [] = []
| del1 A_ a (x :: xs) = (if HOL.eq A_ x a then xs else x :: del1 A_ a xs);
fun delall A_ a [] = []
| delall A_ a (x :: xs) =
(if HOL.eq A_ x a then delall A_ a xs else x :: delall A_ a xs);
However, since this contains some Isabelle specific stuff (like a dictionary construction to get rid of type classes) maybe you prefer hand-written code:
fun del1 a [] = []
| del1 a (x::xs) = if x = a then xs else x :: (del1 a xs)
fun delall a [] = []
| delall a (x::xs) = if x = a then delall a xs else x :: delall a xs
On the other hand, if you just want to try out your functions on some inputs, you can do that inside Isabelle using value
. E.g.,
value "del1 (2::nat) [1, 2 , 3]"
value "delall ''x'' [''x'', ''y'', ''z'', ''q'', ''x'']"