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