author kleing Fri, 16 Apr 2004 09:01:55 +0200 changeset 14581 f56e9e16753b parent 14580 b9fd5e39b695 child 14582 f0779f6fa7e8
updated, tuned
```--- a/Admin/page/main-content/faq.content	Fri Apr 16 08:17:19 2004 +0200
+++ b/Admin/page/main-content/faq.content	Fri Apr 16 09:01:55 2004 +0200
@@ -68,11 +68,11 @@
that takes an element of <tt>a</tt> as input and gives you an
element of <tt>b</tt> as output. The long arrow <tt>--></tt>
and <tt>==></tt> are object and meta level
-        implication. Roughly speaking, the meta level implication is
-        used to write down theorems (<tt>P ==> Q</tt> is a theorem
-        with <tt>P</tt> as premise and <tt>Q</tt> as conclusion), and
-        the object level implication is used in usual HOL formulas
-        (e.g. in definitions).</td></tr>
+        implication. Roughly speaking, the meta level implication
+        should only be used when stating theorems where it separates
+        the assumptions from the conclusion. Whenever you need an
+        implication inside a HOL formula, use <code>--></code>.
+        </td></tr>
</table>

<table class="question" width="100%"><tr><td>Where do I have to put those double quotes?</td></tr></table>
@@ -92,8 +92,8 @@
and <tt>constdefs</tt>)
</td></tr></table>

-    <table class="question" width="100%"><tr><td>What is <tt>No such
-    constant: "_case_syntax"</tt> supposed to tell
+    <table class="question" width="100%"><tr><td>What is <tt>"No such
+    constant: _case_syntax"</tt> supposed to tell
me?</td></tr></table>

<table class="answer" width="100%"><tr><td>You get this message if
@@ -182,22 +182,29 @@

-    <table class="question" width="100%"><tr><td>How do I show
-    counter examples?</td></tr></table>
+    <table class="question" width="100%"><tr><td>Can Isabelle find
+    counterexamples?</td></tr></table>

-    There are a number of commands that try to find counter examples
-    automatically. Try <code>quickcheck</code> for small executable
-    examples and <code>arith</code> for Presburger arithmetic.
+    <p>
+    For arithmetic goals, <code>arith</code> finds counterexamples.
+    For executable goals, <code>quickcheck</code> tries to find a
+    counterexample.  For goals of a more logical nature (including
+    quantifiers, sets and inductive definitions) <code>refute</code>
+    searches for a countermodel.
+    </p>
+    <p>
Otherwise, negate the proposition
and instantiate (some) variables with concrete values. You may