--- a/src/HOL/Hoare/README.html Wed May 01 13:55:20 1996 +0200
+++ b/src/HOL/Hoare/README.html Thu May 02 10:20:15 1996 +0200
@@ -33,4 +33,8 @@
</DL>
The pre/post conditions can be arbitrary HOL formulae including program
variables. The program text should only refer to program variables.
+<P>
+<B>Note</B>: Program variables are typed in the same way as HOL
+variables. Although you can write programs over arbitrary types, all
+program variables in a particular program must be of the same type!
</BODY></HTML>