# HG changeset patch
# User nipkow
# Date 831025215 -7200
# Node ID 7cbff1da8578640d8dce9c43dfe84b2f70915def
# Parent  1a5e0101399de2ba8aaca3b15d464b08fc6fe88e
Added note on types.

diff -r 1a5e0101399d -r 7cbff1da8578 src/HOL/Hoare/README.html
--- 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>