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 @@ The pre/post conditions can be arbitrary HOL formulae including program variables. The program text should only refer to program variables. +

+Note: 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!