--- a/src/Provers/quantifier1.ML Mon Aug 16 16:58:45 2010 +0200
+++ b/src/Provers/quantifier1.ML Mon Aug 16 17:44:27 2010 +0200
@@ -17,7 +17,7 @@
And analogously for t=x, but the eqn is not turned around!
NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
- "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
+ "!x. x=t --> P(x)" is covered by the congruence rule for -->;
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
As must be "? x. t=x & P(x)".
@@ -26,7 +26,7 @@
Gries etc call this the "1 point rules"
The above also works for !x1..xn. and ?x1..xn by moving the defined
-qunatifier inside first, but not for nested bounded quantifiers.
+quantifier inside first, but not for nested bounded quantifiers.
For set comprehensions the basic permutations
... & x = t & ... -> x = t & (... & ...)