# HG changeset patch # User wenzelm # Date 921272571 -3600 # Node ID 643e50fc46bae2f60e1dd3ee6e364ea187f6d936 # Parent c784ab29f424f1b2cb79031832c18d8b0628e7f3 made weblint happy; diff -r c784ab29f424 -r 643e50fc46ba src/HOL/Hoare/README.html --- 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); applies the tactic to subgoal i and applies the parameter -tac (of type int -> tactic) to all generated +tac (of type int -> tactic) to all generated verification conditions. A typical call is
 by(hoare_tac Asm_full_simp_tac 1);
diff -r c784ab29f424 -r 643e50fc46ba src/ZF/AC/README.html
--- 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 @@
 

The report Mechanizing Set Theory, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals. -