[isabelle] Clash of types



Attachment: AExp.thy
Description: Binary data

Attachment: BExp.thy
Description: Binary data

Hi

Attachment: Com.thy
Description: Binary data

Attachment: Hoare.thy
Description: Binary data

I have a problem of clash of types in My Hoare.thy file and i don’t know why ?
the problem is that i expected that p should be of type bexp but it is of type bool in output ??


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