summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Provers/quantifier1.ML

changeset 38457 | b8760b6e7c65 |

parent 38452 | abc655166d61 |

parent 38456 | 6769ccd90ad6 |

child 42361 | 23f352990944 |

--- a/src/Provers/quantifier1.ML Tue Aug 17 12:49:43 2010 +0200 +++ b/src/Provers/quantifier1.ML Tue Aug 17 13:10:58 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 & (... & ...)