Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project!

## Diff of /doc/source/logic_tricks.txt[5b9ac5] .. [ed186b] Maximize Restore

### Switch to side-by-side view

```--- a/doc/source/logic_tricks.txt
+++ b/doc/source/logic_tricks.txt
@@ -126,32 +126,14 @@

For example: for all \$x from generate_x(\$x), test_y(\$x) is true

-Rethink this as a combination of two negatives on ``exists``, above: there
-does *not* ``exist`` an ``\$x`` from ``generate_x(\$x)`` where ``test_y(\$x)`` is
-*not* true.  Then combine the ``not`` trick with the ``exists`` trick.
-This needs a new subgoal, we'll call it ``for_all_x``::
+Use the forall clause::

-    for_all_x_failure:
-        use for_all_x()
-        when
-            generate_x(\$x)          # these two lines are the exists trick
-            not_test_y(\$x)
-            special.claim_goal()    # don't use any other rules for for_all_x
-            check False             # and cause this rule to fail, which causes the for_all_x goal to fail
+    forall
+        generate_x(\$x)
+    require
+        test_y(\$x)

-    for_all_x_success:
-        use for_all_x()             # we only make it here if all generated \$x values have test_y(\$x) true
+Note that all pattern variable bindings done in the forall clause are undone
+before the next clause is run.

-Then you also need to create rules for the ``not_test_y`` goal using the
-``not`` trick, above::
-
-    not_test_y_fail:
-        use not_test_y(\$x)
-        when
-            test_y(\$x)              # if there is any way for test_y(\$x) to be true
-            special.claim_goal()    # don't use any other rules for not_test_y
-            check False             # and cause this rule to fail, which causes the not_test_y goal to fail
-
-    not_test_y_success:
-        use not_test_y(\$_)          # this rule only runs if test_y(\$x) fails, above
-
+This always fails on backtracking.
```