[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?
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