# [isabelle] all Re: [Fwd: Re: Qualified name for Set.insert]

`I think a related issue is that it is not possible to use the identifier
``'all', e.g., I wanted to have the list function
`
primrec all :: "('a => bool) => 'a list => bool"
where "all p [] = True"
| "all p (x#xs) = (p x \<and> all p xs)"

`The definition ran through... however, at some later point I tried to
``use a formula of the form "!!x. ?P x" and there I got a type error.
``Would this problem also be solved if the internal constant for `!!'
``would be qualified... or is it a different problem?
`
cheers
chris
P.S.: is there some workaround that lets me use the function name 'all'?

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*