src/HOL/Hoare/README.html
changeset 1715 7cbff1da8578
parent 1335 5e1c0540f285
child 5646 7c2ddbaf8b8c
--- 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>