Added note on types.
authornipkow
Thu, 02 May 1996 10:20:15 +0200
changeset 1715 7cbff1da8578
parent 1714 1a5e0101399d
child 1716 8dbf9ca61ce5
Added note on types.
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>