# HG changeset patch
# User nipkow
# Date 1082206281 -7200
# Node ID 603f08285c6586934a4c84f9049ecfc101f14539
# Parent  196ff8d245bfe1b37d8f48d5ee891d15a01831c7
small additions

diff -r 196ff8d245bf -r 603f08285c65 Admin/page/main-content/index.content
--- a/Admin/page/main-content/index.content	Sat Apr 17 14:51:00 2004 +0200
+++ b/Admin/page/main-content/index.content	Sat Apr 17 14:51:21 2004 +0200
@@ -58,11 +58,15 @@
 <li><code>arith</code> now generates counterexamples for reals as well.</li>
 
 <li>New <code>quickcheck</code> command
-    to search for counterexamples of executable goals.</li>
+    to search for counterexamples of executable goals.
+  (see HOL/ex/Quickcheck_Examples.thy)</li>
 <li>New <code>refute</code> command
-    to search for finite countermodels of goals.</li>
+    to search for finite countermodels of goals.
+  (see HOL/ex/Refute_Examples.thy)
+</li>
 
-<li>Presentation and x-symbol enhancements, greek letters and sub/superscripts in identifiers.</li>
+<li>Presentation and x-symbol enhancements, greek letters and
+sub/superscripts allowed in identifiers.</li>
 </ul>
 <a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a>
 <p>