[ProofPower] Confused about Z and HOL terms

[Rob Arthan]

On Friday 14 May 2004 11:29 am, Rob Arthan wrote:
>.... For example in something like:
>
> 	[x : X | A = (B /\ C) /\ D]
>
> "A = (B /\ D) /\ C" and "C" are predicates, but "A" and "B /\ C" are
> expressions. 

Whoops! That should read:

"A = (B /\ D) /\ C" and "D" are predicates, but "A" and "B /\ C" are
expressions. 

Regards,

Rob.