--- a/src/HOL/Hoare/README.html Fri Mar 12 18:49:02 1999 +0100
+++ b/src/HOL/Hoare/README.html Fri Mar 12 22:02:51 1999 +0100
@@ -41,7 +41,7 @@
by(hoare_tac tac i);
</PRE>
applies the tactic to subgoal <kbd>i</kbd> and applies the parameter
-<kbd>tac</kbd> (of type <kbd>int -> tactic</kbd>) to all generated
+<kbd>tac</kbd> (of type <kbd>int -> tactic</kbd>) to all generated
verification conditions. A typical call is
<PRE>
by(hoare_tac Asm_full_simp_tac 1);
--- a/src/ZF/AC/README.html Fri Mar 12 18:49:02 1999 +0100
+++ b/src/ZF/AC/README.html Fri Mar 12 22:02:51 1999 +0100
@@ -17,7 +17,6 @@
<P>
The report
<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">Mechanizing Set Theory</A>, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals.
-<P>
</body>
</html>